Integrating action systems and Z in a medical system specification

Abstract

Action systems and the specification language Z, are integrated and used to give different aspects of a single systems specification. The static part of the system under development, i.e., the state declarations together with their accompanying invariants, are first specified using Z. Then the reactivity and real time aspects of the same system are specified within the action systems framework making use of the Z definitions. Furthermore, Z style is used to specify the actions in the action system. We exemplify the proposed methodology through a case study on a medical system specification.