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.

• Type: Conference
• Year: 2008
• Where: CADE
• Authors: Niusha Hakimipour, Paul A. Strooper, Roger Duke
• Keywords: Automated Reasoning, CADE 2008, Current Real-time Model-checking, Model-checking Tools, Real-time Systems