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.
Asynchronous router specification
IEEE Aerospace and Electronic Systems Magazine ; 12 , 3 ; 38-44
1997-03-01
736658 byte
Aufsatz (Zeitschrift)
Elektronische Ressource
Englisch