Integrating Z with Dynamic Modeling Techniques for the Specification of Reactive Systems

. We describe how Z can be combined with dynamic modelling techniques such as Statecharts and temporal interval logic. The presented formalism, #SZ, integrates Z's power to describe data and data-transformation with techniques and an adequate semantic model for reactive systems. #SZ also de#nes powerful means of structuring a speci#cation. The formalism is introduced in presenting parts of the speci#cation of an intelligent cruise control. 1 Introduction Applying formal techniques to the development of safety-critical reactive systems is promising, since the proper function of these systems is important enough to spend possible extra e#ort induced by a formal approach. A framework for applying formal techniques to reactive systems has been developed in the context of the Espress project 1 . In this paper, we describe the design of the speci#cation formalism, #SZ , as it us used in Espress. #SZ combines Z's expressivepower to describe data and data-transformations with the dyn..