Aspects of Continuous Behaviour - Design of Real-Time Reactive Systems in DisCo

Reactive systems, i.e. those in constant interaction with their environments, are often distributed entailing concurrency. Real time is a continuous quantity used to model timing constraints of reactive systems. Developing real-time reactive systems is a battle against complexity. To win this battle methods are needed which support the specification process as well as the validation and verification of specifications. In this thesis an approach concentrating on these important development phases is presented. The foundation of the approach is DisCo which is a formal method for distributed reactive systems. The formal basis of DisCo is in the Temporal Logic of Actions by Lamport. At the core of DisCo are the joint action theory and the closed system principle enabling capturing of collective behaviour of objects before defining their interfaces. Moreover, layered design based on superposition enables effective separation of concerns. The approach contributes to the specification of real-time systems by introducing generic real-time events and a mechanism for their utilization in specifications. Furthermore, the structuring of specifications is elaborated in the light of aspect-orientation, a methodology inspired by the identification of cross-cutting design concerns that do not fit into any single existing unit of modularity, for instance a class. Moreover, the constructs for modelling real time can be generalized to other continuous quantities as well. An example is presented where locations of mobile devices are also of concern. To advance the development of not only well structured but also correct specifications, tools for validation of real-time specifications are presented. A mapping from finite instantiations of DisCo specifications into timed automata is also described. The mapping enables automatic verification of real-time specifications using an existing model checking tool.