The aim of this project is to bring together researchers from the ﬁeld 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.
This project has been supported 2010-2011 by the DAAD ppp programme under the project ID 50727668.
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 ﬁnd 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 speciﬁcation formalism of these tools ensures that interesting properties are decidable, they do not support well the speciﬁcation 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 speciﬁcation, 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.