Formal specification and verification of communication protocols using automated tools

Milica Barjaktarovic; Shiu Kai Chin; Kamal Jabbour

Formal specification and verification of communication protocols using automated tools

Milica Barjaktarovic, Shiu Kai Chin, Kamal Jabbour

Research output: Chapter in Book/Entry/Poem › Conference contribution

Abstract

This 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.

Original language	English (US)
Title of host publication	Proceedings of the IEEE International Conference on Engineering of Complex Computer Systems, ICECCS
Publisher	IEEE Computer Society
Pages	246-253
Number of pages	8
State	Published - 1995
Externally published	Yes
Event	Proceedings of the 1995 1st IEEE International Conference on Engineering of Complex Computer Systems - Ft.Lauderdale, FL, USA Duration: Nov 6 1995 → Nov 10 1995

Other

Other	Proceedings of the 1995 1st IEEE International Conference on Engineering of Complex Computer Systems
City	Ft.Lauderdale, FL, USA
Period	11/6/95 → 11/10/95

ASJC Scopus subject areas

General Computer Science
General Engineering

Cite this

Barjaktarovic, M, Chin, SK & Jabbour, K 1995, Formal specification and verification of communication protocols using automated tools. in Proceedings of the IEEE International Conference on Engineering of Complex Computer Systems, ICECCS. IEEE Computer Society, pp. 246-253, Proceedings of the 1995 1st IEEE International Conference on Engineering of Complex Computer Systems, Ft.Lauderdale, FL, USA, 11/6/95.

@inproceedings{3eedd55d79d145cd9cfe2c39cb005ee3,

title = "Formal specification and verification of communication protocols using automated tools",

abstract = "This 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.",

author = "Milica Barjaktarovic and Chin, {Shiu Kai} and Kamal Jabbour",

year = "1995",

language = "English (US)",

pages = "246--253",

booktitle = "Proceedings of the IEEE International Conference on Engineering of Complex Computer Systems, ICECCS",

publisher = "IEEE Computer Society",

address = "United States",

note = "Proceedings of the 1995 1st IEEE International Conference on Engineering of Complex Computer Systems ; Conference date: 06-11-1995 Through 10-11-1995",

}

TY - GEN

T1 - Formal specification and verification of communication protocols using automated tools

AU - Barjaktarovic, Milica

AU - Chin, Shiu Kai

AU - Jabbour, Kamal

PY - 1995

Y1 - 1995

N2 - This 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.

AB - This 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.

UR - http://www.scopus.com/inward/record.url?scp=0029510021&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=0029510021&partnerID=8YFLogxK

M3 - Conference contribution

AN - SCOPUS:0029510021

SP - 246

EP - 253

BT - Proceedings of the IEEE International Conference on Engineering of Complex Computer Systems, ICECCS

PB - IEEE Computer Society

T2 - Proceedings of the 1995 1st IEEE International Conference on Engineering of Complex Computer Systems

Y2 - 6 November 1995 through 10 November 1995

ER -

Formal specification and verification of communication protocols using automated tools

Abstract

Other

ASJC Scopus subject areas

Other files and links

Fingerprint

Cite this