Formal specification and verification of communication protocols using automated tools

Ft. Lauderdale, Florida November 06-November 10

DOI Bookmark:

http://doi.ieeecomputersociety.org/10.1109/ICECCS.1995.479337

First IEEE International Conference o ...

	This Article
	PURCHASE ARTICLE: $19 PDF HTML IEEE Xplore Subscribers
	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 M. Barjaktarovic Articles by Shiu-Kai Chin Articles by K. Jabbour

	ASCII Text	x
	M. Barjaktarovic, Shiu-Kai Chin, K. Jabbour, "Formal specification and verification of communication protocols using automated tools," Engineering of Complex Computer Systems, IEEE International Conference on, pp. 246, First IEEE International Conference on Engineering of Complex Computer Systems (ICECCS'95), 1995.

	BibTex	x
	@article{ 10.1109/ICECCS.1995.479337, author = {M. Barjaktarovic and Shiu-Kai Chin and K. Jabbour}, title = {Formal specification and verification of communication protocols using automated tools}, journal ={Engineering of Complex Computer Systems, IEEE International Conference on}, volume = {0}, year = {1995}, isbn = {0-8186-7123-8}, pages = {246}, doi = {http://doi.ieeecomputersociety.org/10.1109/ICECCS.1995.479337}, publisher = {IEEE Computer Society}, address = {Los Alamitos, CA, USA}, }

	RefWorks Procite/RefMan/Endnote	x
	TY - CONF JO - Engineering of Complex Computer Systems, IEEE International Conference on TI - Formal specification and verification of communication protocols using automated tools SN - 0-8186-7123-8 SP EP A1 - M. Barjaktarovic, A1 - Shiu-Kai Chin, A1 - K. Jabbour, PY - 1995 KW - formal specification; software tools; protocols; modelling; formal logic; algebra; open systems; theorem proving; testing; simulation; formal specification; formal verification; communication protocols; automated tools; validation; process algebra; OSI protocol; model checker; model testing; complex models; large models; automated theorem prover VL - 0 JA - Engineering of Complex Computer Systems, IEEE International Conference on ER -

M. Barjaktarovic, Dept. of Electr. & Comput. Eng., Wilkes Univ., PA, USA

Shiu-Kai Chin, Dept. of Electr. & Comput. Eng., Wilkes Univ., PA, USA

K. Jabbour, Dept. of Electr. & Comput. Eng., Wilkes Univ., PA, USA

The paper compares and contrasts various methods presently available for specification, validation and verification, with emphasis on verification. We describe an application of formal methods to protocol specification, validation, and verification, using an actual protocol as an example. We use a process algebra to build models of an OSI protocol and test these models using a model checker. Model checking allows us to verify large and complex models and use formal methods as practical solutions. We also show an example with an automated theorem prover.

Index Terms:

formal specification; software tools; protocols; modelling; formal logic; algebra; open systems; theorem proving; testing; simulation; formal specification; formal verification; communication protocols; automated tools; validation; process algebra; OSI protocol; model checker; model testing; complex models; large models; automated theorem prover

Citation:

M. Barjaktarovic, Shiu-Kai Chin, K. Jabbour, "Formal specification and verification of communication protocols using automated tools," iceccs, pp.246, First IEEE International Conference on Engineering of Complex Computer Systems (ICECCS'95), 1995

Peer Review Notice | Give Us Feedback

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