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

Hakimipour, Niusha, Strooper, Paul and Duke, Roger (2008). Exploring model-based development for the verification of real-time Java code. In: Bernhard Beckert and Gerwin Klein, IJCAR 2008: 4th International Joint Conference on Automated Reasoning. Workshop Program: 5th International Verification Workshop. VERIFY’08. VERIFY'08: 5th International Verification Workshop, in connection with IJCAR 2008: The 4th International Joint Conference on Automated Reasoning, Sydney, NSW, Australia, (71-81). 10-15 August, 2008.

Attached Files (Some files may be inaccessible until you login with your UQ eSpace credentials)
Name Description MIMEType Size Downloads
UQ176428_OA.pdf Full text (open access) application/pdf 192.18KB 0
Author Hakimipour, Niusha
Strooper, Paul
Duke, Roger
Title of paper Exploring model-based development for the verification of real-time Java code
Conference name VERIFY'08: 5th International Verification Workshop, in connection with IJCAR 2008: The 4th International Joint Conference on Automated Reasoning
Conference location Sydney, NSW, Australia
Conference dates 10-15 August, 2008
Proceedings title IJCAR 2008: 4th International Joint Conference on Automated Reasoning. Workshop Program: 5th International Verification Workshop. VERIFY’08   Check publisher's open access policy
Journal name CEUR Workshop Proceedings   Check publisher's open access policy
Place of Publication Aachen, Germany
Publisher Lehrstuhl Informatik V, Rheinisch-Westfaelische Technische Hochschule Aachen
Publication Year 2008
Sub-type Fully published paper
ISSN 1613-0073
Editor Bernhard Beckert
Gerwin Klein
Volume 372
Start page 71
End page 81
Total pages 11
Collection year 2009
Language eng
Formatted Abstract/Summary
Many safety- and security-critical systems are real-time systems and, as a result, tools and techniques for verifying real-time systems 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. However, they provide formal verification for models, not programs. To increase the confidence in real-time programs written in real-time Java, this paper takes a modelling approach to the design 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. To illustrate the approach we use a nontrivial example: a gear controller.
Subjects E1
890299 Computer Software and Services not elsewhere classified
080309 Software Engineering
Q-Index Code E1
Q-Index Status Confirmed Code

 
Versions
Version Filter Type
Citation counts: Scopus Citation Count Cited 0 times in Scopus Article
Google Scholar Search Google Scholar
Created: Thu, 16 Apr 2009, 16:48:28 EST by Ms Kimberley Nunes on behalf of School of Information Technol and Elec Engineering