A model-based development approach for the verification of 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. Simulation 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. Although they provide formal verification for models, we still need to implement these models. To increase the confidence in real-time programs written in real-time Java, this paper 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 can be derived from the model by following a systematic approach. We introduce a timed automata to RTSJ Tool (TART), a prototype tool to automatically generate real-time Java code from the model. Finally, we show the applicability of our approach by means of four examples: a gear controller, an audio/video protocol, a producer/consumer and the Fischer protocol. Copyright © 2011 John Wiley & Sons, Ltd.