Sciweavers

Share
CADE
2008
Springer

Exploring Model-Based Development for the Verification of Real-Time Java Code

9 years 2 months ago
Exploring Model-Based Development for the Verification of Real-Time Java Code
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.
Niusha Hakimipour, Paul A. Strooper, Roger Duke
Added 03 Dec 2009
Updated 03 Dec 2009
Type Conference
Year 2008
Where CADE
Authors Niusha Hakimipour, Paul A. Strooper, Roger Duke
Comments (0)
books