Modeling and Verifying Real-time Properties of Reactive Systems

SPACE is a model-driven engineering technique for reactive distributed systems. It enables to develop system models from reusable building blocks, formal analysis by model checking as well as automated transformation to executable code. In this paper, we describe an extension of the SPACE formalism which allows to model and verify also real-time behavior. In particular, one specifies real-time constraints in the interface descriptions of the building blocks, so-called Real-Time External State-Machines (RTESMs). The RTESMs are translated to guards, clocks and invariants of Timed Automata which can be analyzed by means of the model checker UPPAAL. The approach is explained by a component protecting an electrical motor controller system against overspeed. In particular, we prove that by keeping certain maximum response times, this system guarantees that the speed of the motor stays within certain limits.