| Abstract: | 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. |
