Submodule construction as equation solving in CCS

In top-down design methodologies the following problem arises: given specifications of a system and some of its submodules, derive a specification for the remaining submodules. We formulate this problem in CCS as an equation (A|X)⧹L ≈ B, where X is unknown, B represents the whole system, A the known submodules, and L the channels over which the submodules interact. We present a procedure for solving such equations by successive transformation of equations into simpler equations in parallel with generation of a solution. The procedure has been implemented as a semiautomatic program, where the user may interact in order to guide the transformations towards particular solutions. As an example we demonstrate the automatic generation of receivers of two versions of the Alternating Bit protocol.

Authors

• Joachim Parrow

Keywords

No keywords are indexed for this paper.