Keywords: hybrid systems, embedded systems, real time, formal methods, specification, verification, hybrid automata, timed automata, temporal logics, symbolic model checking
Start Date: 1 November 94 / Duration: 36 months
[ participants / contact]
Embedded systems are increasingly prevalent in areas such as avionics, process control, communications, and robotics. Most of these are hybrid systems in that they combine the processing of continuous and discrete data, and operate and interact in real time with a continuously changing environment. The analysis and prediction of the behaviour of such systems require formal methods and tools to support these methods. This project focuses on a symbolic model checking approach to the verification of hybrid systems by extending the KRONOS tool developed at VERIMAG.
During the last year, two algorithms have been developed and implemented to extend the capabilities and to improve the performances of the verification tool KRONOS. The first one is based on symbolic forward reachability analysis of the state space. The second one constructs the coarsest partition of the set of reachable states with respect to a time-abstracting bisimulation. These algorithms have been successfully applied to verify realistic case studies.
The experimental results obtained with KRONOS, concerning the verification of timing properties of circuits and protocols, led to contacts with industrial research laboratories at Intel (USA) and CNET (France). A one-week seminar was organised by InCo in December 1995 in the course of the "Jornadas Uruguayas de Informatica 1995". A one-semester course on specification and verification of real-time and hybrid systems has now become part of the computer science degree at InCo, Universidad de la Republica, Uruguay. KRONOS was presented during the tool demonstration session at the 8th Conference on Computer-Aided Verification, CAV'96, Rutgers, NJ, USA.
38330 Montbonnot, F
University of Crete, GR
Instituto de Computacion, UY
Dr. Sergio Yovine
Tel: +33 76 90 96 41
Fax: +33 76 41 36 20
HYBSYS - KIT139, May 1997
please address enquiries to the ESPRIT Information Desk
html version of synopsis by Nick Cook