Automated Formal Verification of Protocols

	This Article
	Subscribers, please Login Purchase article: $19 PDF IEEE Xplore Subscribers RSS feed
	Share
	Email this Article to a friend
	Bibliographic References
	ASCII Text BibTex RefWorks Procite/RefMan/Endnote
	Add to:
	Digg Furl Spurl Blink Simpy Google Del.icio.us Y!MyWeb
	Search
	Similar Articles Articles by D. R. Avresky Articles by S. Vassilaras

Sixth International Conference on Computer Communications and Networks (ICCCN '97)

Las Vegas, NV

September 22-September 25

ISBN: 0-8186-8186-1

	ASCII Text	x
	D. R. Avresky, S. Vassilaras, "Automated Formal Verification of Protocols," Computer Communications and Networks, International Conference on, pp. 166, Sixth International Conference on Computer Communications and Networks (ICCCN '97), 1997.

	BibTex	x
	@article{ 10.1109/ICCCN.1997.623308, author = {D. R. Avresky and S. Vassilaras}, title = {Automated Formal Verification of Protocols}, journal ={Computer Communications and Networks, International Conference on}, volume = {0}, year = {1997}, issn = {1095-2055}, pages = {166}, doi = {http://doi.ieeecomputersociety.org/10.1109/ICCCN.1997.623308}, publisher = {IEEE Computer Society}, address = {Los Alamitos, CA, USA}, }

	RefWorks Procite/RefMan/Endnote	x
	TY - CONF JO - Computer Communications and Networks, International Conference on TI - Automated Formal Verification of Protocols SN - 1095-2055 SP EP A1 - D. R. Avresky, A1 - S. Vassilaras, PY - 1997 KW - Formal methods KW - telecommunication protocols KW - real-time systems KW - execution tree VL - 0 JA - Computer Communications and Networks, International Conference on ER -

D. R. Avresky, Department of Electrical Engineering Boston University

S. Vassilaras, Department of Electrical Engineering Boston University

DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/ICCCN.1997.623308

We adopt a formalism to describe protocols that is close to the human way of thinking and can be easily used to perform reachability analysis of the described protocol in a state-transition format. This formalism allows for an execution tree (ET) to be generated from a set of assertions such that all paths from the root to the leaves are well-defined formulas. We then extend the formalism with regards to real-time properties. Finally, we present a software verification tool, Verify, that implements the above features in the analysis of protocols.

Index Terms:

Formal methods, telecommunication protocols, real-time systems, execution tree

Citation:

D. R. Avresky, S. Vassilaras, "Automated Formal Verification of Protocols," icccn, pp.166, Sixth International Conference on Computer Communications and Networks (ICCCN '97), 1997

Peer Review Notice | Give Us Feedback

Usage of this product signifies your acceptance of the Terms of Use.