TY - JOUR
T1 - A model-based development approach for the verification of real-time Java code
AU - Wellings, Andy
AU - Hakimi Pour, Niusha
AU - Strooper, Paul
PY - 2011/9/10
Y1 - 2011/9/10
N2 - 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.
AB - 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.
UR - http://www.scopus.com/inward/record.url?scp=80051784148&partnerID=8YFLogxK
U2 - DOI: 10.1002/cpe.1728
DO - DOI: 10.1002/cpe.1728
M3 - Article
SN - 1532-0634
VL - 23
SP - 1583
EP - 1606
JO - Concurrency and Computation: Practice and Experience
JF - Concurrency and Computation: Practice and Experience
IS - 13
ER -