Reactive system specification and refinement

Abstract

This paper describes formal approaches for reactive and real time system specification and development, using a process of systematic translation from statechart descriptions of a system into a specification language utilising real time logic (RTL), and refinement within this language. Alternative implementation strategies using synchronisation constraints and synchronisation code are also provided, together with examples of development using the approach. The approach provides a unitary formalism which combines statecharts, RTL and temporal logic. Animation and proof tools are also briefly described.