Hybrid Systems Modeling and Analysis with Rewriting Techniques

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. Su ch real-time systems are often critical systems that must be well understood before deployment. The use of formal methods has been advocated to define a precise yet high-level mathematical model of the design of a complex system that can be subjected to different kinds of (machine-assisted or entirely automated) mathematical analyses to find errors in the design and/or to prove the design correct. The aim of this project is to bring together researchers from the University of Oslo and RWTH Aachen in or der to develop new techniques for modeling and analyzing advanced real-time and hybrid systems that are beyond the pale of existing formal tools for real-time and hybrid systems. In addition to the more immediate scientific goals of this project, we envi sage that the proposed project leads to a collaboration on a broader basis between the two groups in the future, for instance on the crucial task of combining timed and probabilistic reasoning for object-oriented systems.