A model-based development approach for the verification of real-time Java code

Hakimi Pour, Niusha, Strooper, Paul and Wellings, Andy (2011) A model-based development approach for the verification of real-time Java code. Concurrency and Computation: Practice and Experience, 23 13: 1583-1606. doi:10.1002/cpe.1728


Author Hakimi Pour, Niusha
Strooper, Paul
Wellings, Andy
Title A model-based development approach for the verification of real-time Java code
Journal name Concurrency and Computation: Practice and Experience   Check publisher's open access policy
ISSN 1040-3108
1532-0626
1532-0634
Publication date 2011-09-10
Sub-type Article (original research)
DOI 10.1002/cpe.1728
Volume 23
Issue 13
Start page 1583
End page 1606
Total pages 24
Place of publication Bognor Regis, West Sussex, U.K.
Publisher John Wiley & Sons
Collection year 2012
Language eng
Formatted 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.
Keyword RTSJ
Formal verification
Model-based approach
Q-Index Code C1
Q-Index Status Confirmed Code
Institutional Status UQ

Document type: Journal Article
Sub-type: Article (original research)
Collections: Official 2012 Collection
School of Information Technology and Electrical Engineering Publications
 
Versions
Version Filter Type
Citation counts: TR Web of Science Citation Count  Cited 0 times in Thomson Reuters Web of Science Article
Scopus Citation Count Cited 2 times in Scopus Article | Citations
Google Scholar Search Google Scholar
Created: Fri, 13 May 2011, 14:19:54 EST by Ms Niusha Hakimipour on behalf of School of Information Technol and Elec Engineering