Integrated Environments for Formally Weil-Founded Design and Simulation of Concurrent Systems

We describe an ongoing project concerned with the systematic development of environments that support the specification and design of concurrent systems. The project has two key aspects: an existing and working system, Clara, that supports Milner's CCS as a specification and design language; and the development of general techniques for computer-aided generation of Clara-like environments for other concurrent languages. In this paper, we focus on the Clara environment. The Clara environment has two main components: 1) support for the usage of formal techniques in the design process, and 2) a rich and highly interactive simulation facility. A further distinguishing feature is the environment's graphical user interface which is based on a pictorial version of CCS. CCS is one of the most promising formalisms for defining concurrent systems and has been used successfully in many practical applications. This makes an environment that supports the calculus attractive in its own right. Moreover, the semantics of CCS is defined nonprocedural!) in two phases: an operational semantics given as a set of inference rules, and then an algebraic semantics represented by a set of equational rules. This nonprocedural representation of formal semantics constitutes the foundation of our strategy for exporting the functionalities of Clara to its “clone environments.”