HYBSYS

HYBSYS - KIT139

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]

Objectivies and Approach

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.

Progress and Results

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.

Information Dissemination Activities and/or Exploitation

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.

Coordinator

VERIMAG
Rue Lavoisier
38330 Montbonnot, F

EU Partners

VERIMAG, F
University of Crete, GR

Non-EU Partners

Instituto de Computacion, UY

CONTACT POINT

Dr. Sergio Yovine
Tel: +33 76 90 96 41
Fax: +33 76 41 36 20
E-mail: Sergio.YOVINE@imag.fr
WWW: http://www.imag.fr/VERIMAG