From verified real-time models to real-time Java code

Many real-time systems are safety- and security-critical systems and, as a result, tools and techniques for verifying them are extremely important. Simulating and testing such systems can be exceedingly time-consuming and these techniques provide only probabilistic measures of correctness. There are a number of model-checking tools for real-time systems. However, after they provide formal verification for models, we still need to have a systematic approach for deriving programs from those models. To increase the confidence in real-time programs written in real-time Java, this thesis proposes a model-based approach to the development of such programs. First, models can be mechanically verified, to check whether they satisfy particular properties, by using current real-time model-checking tools. Then, programs are derived from the model by following a systematic approach. Following this approach we can guarantee that all safety and bounded liveness (not liveness in general) properties that are satisfied in the model are also satisfied in the generated code if the target platform meets our conditions (for timing invariants in the model, we need to perform an independent check on the generated code to ensure that the timing invariants are satisfied for the target platform on which the code is executed). To facilitate better timing analysis at the code level, we provide architectural templates for the main abstractions found in real-time systems (periodic, sporadic, and aperiodic). Hence we can provide scheduling analysis techniques if these templates are used. Although memory management is a crucial issue for real-time systems, model checkers usually only provide simple data structures (to avoid state explosion). In our approach we do not deal with memory allocation. Memory allocation will be performed after the code has been generated. We introduce a Timed Automata to RTSJ Tool (TART), a prototype tool to automatically generate real-time Java code from models. We apply our approach on a number of case studies (Fischer protocol, a gear controller, a producer/consumer and an audio/video protocol) to illustrate our mapping, and to show its applicability as well as its limitations