Design and validation of a message-passing system

Author

Lin, Fuyau

Author_Institution

Dept. of Comput. Eng., Santa Clara Univ., CA, USA

fYear

1993

fDate

6-7 Dec 1993

Firstpage

10

Lastpage

19

Abstract

The paper describes a case study for designing and validating the core of a message-passing communication system. The approach is based on the use of the Petri Net Workbench, the protocol validation language, PROMELA, and its simulator/validator, SPIN. By using these tools, a protocol and underlying hardware for communicating between two heterogeneous computer systems is designed and validated. A reachability analysis is performed which includes a check for live- and dead-lock system states.

Keywords

Petri nets; concurrency control; formal verification; message passing; protocols; specification languages; PROMELA; Petri Net Workbench; SPIN; case study; dead-lock system states; heterogeneous computer systems; live-lock system states; message-passing communication; message-passing system; protocol validation language; reachability analysis; simulator/validator; underlying hardware; Application software; Communication system software; Computational modeling; Computer networks; Design engineering; Hardware; Problem-solving; Protocols; Reachability analysis; Software performance;

fLanguage

English

Publisher

ieee

Conference_Titel

Software Specification and Design, 1993., Proceedings of the Seventh International Workshop on

Print_ISBN

0-8186-4360-9

Type

conf

DOI

10.1109/IWSSD.1993.315519

Filename

315519