A Practical Combination of a Process Algebra with an Algebraic Specification Language

摘要

In our approach, we suggest a formal framework as a basis for a generic combination of formal languages. It makes it possible the developer to specify the dynamic part of a system with a process algebra, and the static part with an algebraic specification language. The framework rests on a formal kernel composed of an abstract grammar describing the general form of the combination, and a global operational semantics giving the meaning of each language which can be built with our framework. In this paper, we focus on the practical use of the theoretical aspects of this work. More precisely, we detail in which way the framework could be the basis of the specification of a real size case study. Furthermore, we show how existing tools are reused to partially tackle the verification aspects.