Combining statecharts and Z for the design of safety-critical control systems

Abstract

In this report, we describe an approach that integrates a mathematical specification language with more traditional software design techniques to yield a practicable methodology for the specification of safety-critical control systems. To manage complexity and to foster separation of concerns, the system design model is divided into three views: the architectural view, specified with object and class diagrams; the reactive view, specified with statecharts; and the functional view, specified with Z. A systematic relationship between the reactive and the functional view entails proof obligations to guarantee semantic compatibility. We illustrate this approach with a case study on controlling a heavy hydraulic press.