Hybrid Systems Modeling and Analysis with Rewriting Techniques (HySmart)

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.

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 ﬁ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.

2015
[bibtex]	Daniela Lepri, Erika Abraham, Peter Csaba Ölveczky. Sound and Complete Timed CTL Model Checking of Timed Kripke Structures and Real-Time Rewrite Theories. Science of Computer Programming 99, pages 128–192, 2015.
[bibtex]	Muhammad Fadlisyah, Peter Csaba Ölveczky, Erika Abraham. Formal Modeling and Analysis of Interacting Hybrid Systems in HI-Maude: What Happened at the 2010 Sauna World Championships?. Science of Computer Programming 99, pages 95–127, 2015.
2013
[bibtex]	Daniela Lepri, Erika Abraham, Peter Csaba Ölveczky. A Timed CTL Model Checker for Real-Time Maude. Proc. of the 5th Int. Conf. on Algebra and Coalgebra in Computer Science (CALCO'13), Volume 8089 of LNCS, pages 334–339, Springer-Verlag, 2013.
2012
[bibtex]	Daniela Lepri, Erika Abraham, Peter Csaba Ölveczky. Timed CTL Model Checking in Real-Time Maude. Proc. of the 9th Int. Workshop on Rewriting Logic and its Applications (WRLA'12), Volume 7571 of LNCS, pages 182–200, Springer Berlin Heidelberg, 2012.
[bibtex]	Muhammad Fadlisyah, Peter Csaba Ölveczky, Erika Abraham. Formal Modeling and Analysis of Human Body Exposure to Extreme Heat in HI-Maude. Proc. of the 9th Int. Workshop on Rewriting Logic and its Applications (WRLA'12), Volume 7571 of LNCS, pages 139–161, Springer Berlin Heidelberg, 2012.
2011
[bibtex]	Muhammad Fadlisyah, Peter Csaba Ölveczky, Erika Abraham. Adaptive-Step-Size Numerical Methods in Rewriting-Logic-Based Formal Analysis of Interacting Hybrid Systems. Int. Workshop on Harnessing Theories for Tool Support in Software (TTSS'10), Volume 274 of ENTCS, pages 17–32, Elsevier Science Publishers, 2011.
[bibtex]	Muhammad Fadlisyah, Peter Csaba Ölveczky, Erika Abraham. Formal Modeling and Analysis of Hybrid Systems in Rewriting Logic using Higher-Order Numerical Methods and Discrete-Event Detection. Int. Symp. on Computer Science and Software Engineering (CSSE'11), pages 1–8, IEEE, 2011.
[bibtex]	Muhammad Fadlisyah, Peter Csaba Ölveczky, Erika Abraham. Object-Oriented Formal Modeling and Analysis of Interacting Hybrid Systems in HI-Maude. 9th Int. Conf. on Software Engineering and Formal Methods (SEFM'11), Volume 7041 of LNCS, pages 415–430, Springer Berlin Heidelberg, 2011.
2010
[bibtex]	Daniela Lepri, Peter Csaba Ölveczky, Erika Abraham. Model Checking Classes of Metric LTL Properties of Object-Oriented Real-Time Maude Specifications. 1st Int. Workshop on Rewriting Techniques for Real-Time Systems (RTRTS'10), Volume 36 of Electronic Proceedings in Theoretical Computer Science, pages 117–136, Open Publishing Association, 2010.
[bibtex]	Muhammad Fadlisyah, Erika Abraham, Daniela Lepri, Peter Csaba Ölveczky. A Rewriting-Logic-Based Technique for Modeling Thermal Systems. 1st Int. Workshop on Rewriting Techniques for Real-Time Systems (RTRTS'10), Volume 36 of Electronic Proceedings in Theoretical Computer Science, pages 82–100, Cornell University Library, 2010.
[bibtex]	Muhammad Fadlisyah, Erika Abraham, Peter Csaba Ölveczky. Rewriting-Logic-Based Formal Modeling and Analysis of Interacting Hybrid Systems. Nordic Workshop on Programming Theory (NWPT'10), , 2010.