On the parameterized algebraic specification of concurrent systems

A technique for specifying concurrent systems is shown, that uses the algebraic specification language ASL. A system is algebraically specified as a transition system and a concurrent system is the result of composing systems by three basic operations: synchronization, parallel composition and monitoring. These operations are schematically described using the parameterization concept of ASL and they are in the same time examples for the power of ASL since they cannot be formally specified in other specification languages. Each particular synchronization, parallel composition or monitoring is defined by instantiating on appropriate parameters a unique specification, which produces a transition system out of an input transition system. By combining the three operations we obtain a formal support for a methodology of hierarchical and modular specification of concurrent systems. Moreover it is shown that combining tools for defining semantics in ASL with the above parameterized schema provides a standard way for giving to a concurrent system a variety of semantics depending on observability constraints. Mathematical Foundations of Software Development Mathematical Foundations of Software Development Look Inside Other actions Export citations About this Book