Verifying transformations between timed automata specifications and ECA rules

Event-triggered real-time systems are desirable to use in environments where the arrival of events are hard to predict. The semantics of an event-triggered system is well mapped to the behaviour of an active database management system (ADBMS), specified using event-condition-action (ECA) rules. The benefits of using an active database, such as persistent data storage, concurrency control, timely response to event occurrences etc. highlights the need for a development method for event-triggered real-time systems using active databases. However, there are problems left to be solved before an ADBMS can be used with confidence in real-time environments. The behaviour of a real-time system must be predictable, which implies a thorough analysed specification with e.g. specified worst case execution times. The predictability requirement is an obstacle for specifying real-time systems as ECA rules, since the rules may affect each other in many intricate ways which makes them hard to analyse. The interaction between the rules implies that it is not enough to verify the correctness of single rules; an analysis must consider the behaviour of the entire rule set. In this dissertation, an approach for developing active applications is presented. A method is examined which starts with an analysed high-level timed automaton specification and transforms the specified behaviour into an implicitly analysed rule set. For this method to be useful, the transformation from timed automata to rules must preserve the exact behaviour of the high level specification. Hence, the aim of this dissertation is to verify transformations between timed automaton specifications and ECA rules. The contribution of this project is a structured set of general transformations between timed automata specifications and ECA rules. The transformations include both transformations of small timed automata constructs for deterministic environments and formally verified timed automata patterns specifying the behaviour of composite events in recent and chronicle context