An equivalence theorem for the specification of asynchronous communication systems (SACS) and asynchronous message passing systems (AMPS)

Formal semantics have been employed in the specification and verification of programming languages. Language for Implementing Parallel/distributed Systems (LIPS) is an asynchronous message passing parallel programming language which handles communication and computation parts independently. The communication part of LIPS can be specified using a process algebraic tool, Specification of Asynchronous Communication Systems (SACS), and is implemented using Asynchronous Message Passing System (AMPS). An implementation is said to be complete only when we prove that it meets its specifications. To achieve that we need to prove an equivalence relation between a program’s specification and its implementation. This means that it is necessary to study the proof of equivalence of SACS and AMPS to prove the completeness of AMPS. The semantics of both SACS and AMPS have been defined using Structural Operational Semantics (SOS) in terms of Labelled Transition Systems (LTS). So we have two labelled transition system semantics : one for SACS and one for AMPS. In this paper we are proving the bisimilarity of these two labelled transition systems to prove that SACS and AMPS are equivalent.

Also available as an ebook with ISBN = 9789048136605