Title :
The specification of an asynchronous router
Author_Institution :
Dept. of Comput. Sci., Uppsala Univ., Sweden
Abstract :
We describe the application of three formal design tools to a case study in the design of a distributed system. The case study in question involves the specification of an asynchronous message router; the three design tools are process algebra (specifically Milner´s Calculus of Communicating Systems CCS), the modal μ calculus and the Edinburgh Concurrency Workbench (CWB). We demonstrate how an informally presented specification can be formalised within the language of the modal μ calculus, allowing for a rigorous mathematical analysis of the correctness of our proposed implementation. For modest sized versions of the router, this correctness proof has been carried out using the CWB
Keywords :
calculus of communicating systems; formal logic; formal specification; message passing; CCS; CWB; Calculus of Communicating Systems; Edinburgh Concurrency Workbench; asynchronous message router; asynchronous router specification; correctness proof; distributed system; formal design tools; informally presented specification; modal μ calculus; process algebra; rigorous mathematical analysis; Algebra; Calculus; Carbon capture and storage; Circuits; Concurrent computing; Delay; Hardware; Interference; Process design; Safety;
Conference_Titel :
Computer Assurance, 1996. COMPASS '96, Systems Integrity. Software Safety. Process Security. Proceedings of the Eleventh Annual Conference on
Conference_Location :
Gaithersburg, MD
Print_ISBN :
0-7803-3390-X
DOI :
10.1109/CMPASS.1996.507882
