Hybrid Systems Modeling and Analysis with Rewriting Techniques (HySmart)

HySmart

The aim of this project is to bring together researchers from the field of rewriting techniques on the one hand, and hybrid systems on the other hand, to develop new rewriting-based techniques for the modeling and analysis of advanced real-time and hybrid systems beyond the reach of existing formal tools.

Funding

This project has been supported 2010-2011 by the DAAD ppp programme under the project ID 50727668.

Team

  University of Oslo, Norway
      Peter Csaba Ölveczky
      Martin Steffen
      Muhammad Fadlisyah
      Daniela Lepri
  RWTH Aachen University, Germany
     Erika Ábrahám
     Jürgen Giesl
     Carsten Fuhs
     Nils Jansen

Description

The functionality of many modern advanced computer systems – such as medical devices, control systems, embedded automotive and avionics systems, Internet protocols, etc. – is crucially dependent on the amount of time that passes during/between events. Such real-time systems are often critical systems that must be well understood before deployment.
The use of formal methods in the early stages of the system development process has been advocated in order to arrive at a precise yet high-level mathematical model of the design of a complex system. The formal model can then be subjected to different kinds of mathematical analysis – preferably machine-assisted or entirely automated – to find errors in the design and/or to prove the design correct.
Advanced real-time computer systems pose a challenge to modeling formalisms, in that different aspects, such as, e.g., real-time and probabilistic behavior, advanced communication and interaction features, complex and unbounded data types, etc., must be captured. The most popular formal tools for real-time systems (UPPAAL, Kronos, and HyTech) are based on timed or hybrid automata.
While the restrictive specification formalism of these tools ensures that interesting properties are decidable, they do not support well the specification of larger systems with different communication models and advanced object-oriented features. In joint work with José Meseguer at the University of Illinois, Ölveczky has developed the rewriting-logic-based Real-Time Maude formalism and analysis tool. Real-Time Maude can be seen as complementing timed-automaton-based formal tools by emphasizing ease and generality of specification, including support for distributed real-time object-based systems. Real-Time Maude has been successfully applied to a wide range of complex state-of-the-art systems that cannot be modeled using the standard formal real-time tools.
In this project we developed rewriting-logic-based methods for modeling and analysing hybrid systems, and integrated them into the Real-Time Maude.

Publications