HySmart

You have come to an old website. Our new URL is ths.rwth-aachen.de. Please update your bookmarks!

Hybrid Systems Modeling and Analysis with Rewriting Techniques (HySmart)

The aim of this project is to bring together researchers from the ﬁeld of rewrit-
ing techniques on the one hand, and hybrid systems on the other hand, to de-
velop new rewriting-based techniques for the modeling and analysis of ad-
vanced real-time and hybrid systems beyond the reach of existing formal tools.

Persons

Oslo:

Aachen:

Description

The functionality of many modern advanced computer systems – such as med-
ical devices, control systems, embedded automotive and avionics systems, In-
ternet 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 mathe-
matical 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 for-
malisms, in that different aspects, such as, e.g., real-time and probabilistic
behavior, advanced communication and interaction features, complex and un-
bounded 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 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. As mentioned below, 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.

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

BSc/MSc/Diploma Topics
Teaching WS 2012/13
Hybrid Systems Group

We are looking for a HiWi for the Compiler Construction course. If you are interested, please contact Thomas Noll.

Joost-Pieter Katoen has been appointed as a member of the renowned Academia Europaea (Academy of Europe), a European, non-governmental association acting as an Academy whose members are scientists and scholars who collectively aim to promote learning, education and research.

Vacancies for postdoctoral researchers in "Automated Analysis of Probabilistic Programs". Application deadline: August 15, 2013.

Joost-Pieter Katoen has been awarded a Distinguished Professorship from the RWTH Aachen University.

The Hybrid Systems: Computation and Control (HSCC'13) conference in Philadelphia has been very successful: Hongfei Fu received the best student paper award for his paper "Approximating acceptance probabilities of CTMC-paths on multi-clock deterministic timed automata". Besides, the paper by Ilya Tkachev, Alexandru Mereacre, Alessandro Abate and Joost-Pieter Katoen was ranked second in the overall best paper award selection.

Joost-Pieter Katoen has been elected as Steering Committee Chair of ETAPS (www.etaps.org), the largest conference on theory and practice of software in Europe. He is the first non-UK ETAPS SC chair since the conference was initiated in 1998. More information here.

The Alumni-Magazine of RWTH Aachen University contains an interview with our former PhD student and postdoctoral researcher, Dr. Tingting Han.

HiWi's wanted to work in a new European Space Agency project for enhancing state-of-the-art design and analysis tools (COMPASS) for the next generation European rockets. Need programming and model checking affinity. See here for details and contact.

We offer openings for several PhD candidates in the area of
"Model-Based Design and Analysis for Dependable Software Systems". Deadline for application: September 14, 2012. For further information click here.

The Theory of Hybrid Systems Group offers two jobs as student assistants within the CEBug project. For more information, look here.

Dino Distefano received the prestigious Roger Needham Award for his work on software verification. This award is for a distinguished research contribution in computer science by a UK based researcher who has completed up to 10 years of post-doctoral research. Dr. Distefano was the first PhD student supervised by Joost-Pieter Katoen.

Marijn Jongerden received the German MMB (Messung, Modellierung und Bewertung von Rechensystemen) Award 2012 of the GI/ITG-Committee for Measurement, Modelling and Evaluation of Computing Systems for his PhD-thesis on "Model-based energy analysis of battery powered systems". His work was supervised by Boudewijn Haverkort (Twente) and Joost-Pieter Katoen.

Our paper "Formal Correctness, Safety, Dependability and Performance Analysis of a Satellite" has been accepted to ICSE 2012 in the track SE in Practice (18% acceptance rate). The paper treats a new satellite from the European Space Agency that was modeled and analyzed with modern tools during the actual satellite design.

Joost-Pieter Katoen will act as DJ in the "Nacht der Professoren" in the Apollo bar and cinema.