Title :
Design and validation of a message-passing system
Author_Institution :
Dept. of Comput. Eng., Santa Clara Univ., CA, USA
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;
Conference_Titel :
Software Specification and Design, 1993., Proceedings of the Seventh International Workshop on
Print_ISBN :
0-8186-4360-9
DOI :
10.1109/IWSSD.1993.315519
