Systems Level Specification and Modelling of Reactive Systems: Concepts, Methods, and Tools

As part of a comprehensive design concept for complex reactive systems we investigate the derivation of formal requirements and design specifications at systems level. We discuss the meaning of correctness with respect to the embedding of mathematical models into the physical world. A crucial aspect in our attempt to make the logic link between the application domain specific view and the formal view explicit is the concept of evolving algebra [13, 14]; it provides the formal basis of a specification methodology which has successfully been applied to a variety of specification and verification problems. We introduce an evolving algebra abstract machine as a conceptual framework for the development of tools for machine based analysis and execution of evolving algebra specifications