Deriving Software Specifications from Event Based Models

摘要

We present a method to derive sequential program specifications from system models. We use an event based approach to model systems, as it allows us to specify parallel, concurrent and distributed systems. We refine the specification of a system until we have introduced all the events needed by its components to interact with the environment. Then, we derive an environment specification and a specification for each component. We use pre-conditions and post-conditions in these specifications, so that they can be implemented using the classical refinement relation for sequential programs. The derived components share the environment module to interact with each other.