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

Speaker: Niusha Hakimipour

When: 10:00, Friday 5th September 2008

Venue: 78-420

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. Simulating and testing also 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. Model-checking real-time Java code is the main topic of this project. Various approaches for model-checking real-time Java code, such as translating real-time Java code to languages which are supported by current real-time model-checkers or extending current Java model-checkers, will be investigated. As a result of this project, an approach for model-checking systems which are implemented in real-time Java will be proposed.

Hospitality: Paul Strooper and Roger Duke

Contact: Robert Colvin (SSE seminar co-ordinator) (robert@itee.uq.edu.au)

SSE seminar web page: http://www.itee.uq.edu.au/~sse/Seminars.html