Asynchronous router specification

Author

Moller, F.

Author_Institution

Dept. of Comput. Sci., Uppsala Univ., Sweden

Volume

12

Issue

3

fYear

1997

fDate

3/1/1997 12:00:00 AM

Firstpage

38

Lastpage

44

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; concurrency control; formal specification; formal verification; message passing; process algebra; Edinburgh Concurrency Workbench; Milner calculus of communicating systems; asynchronous message router; asynchronous router specification; correctness proof; distributed system design; formal design tools; modal /spl mu/-calculus; process algebra; Algebra; Calculus; Carbon capture and storage; Circuits; Concurrent computing; Delay; Distributed computing; Hardware; Mathematical analysis; Process design;

fLanguage

English

Journal_Title

Aerospace and Electronic Systems Magazine, IEEE

Publisher

ieee

ISSN

0885-8985

Type

jour

DOI

10.1109/62.579208

Filename

579208