Sphinx

Hybrid systems, i.e., systems that can be described in terms of continuous physical evolution and being governed by discrete control structures, are pervasively embedded into our lives. Often, they are implemented as so-called cyber-physical systems: embedded controllers/computers implement discrete control structures on the basis of sensed real-world values, and actuators thereupon manipulate the real, physical world. Prominent examples for such hybrid, cyber-physical systems can be found in the area of road traffic management, air traffic, and railroad control: one such example are adaptive cruise control systems being shipped by essentially every car manufacturer in their top-line models. Such technology, however, would not be particularly useful if it led to vastly sub-optimal or incorrect control decisions, possibly even endangering safety on the road, in planes and trains. One particularly interesting challenge to help develop such next-generation cyber-physical systems, thus, is the question of how to ensure correct functioning and reliability of such a system. For this, modeling, simulation, verification, and, finally, implementation techniques are of paramount importance.

The hybrid systems workbench aims at providing an integrated modeling environment, that combines models for hybrid systems geared towards verification (e.g., hybrid programs expressed in differential dynamic logic) with such that are suitable for simulation and liveness verification (e.g., hybrid Petri nets). Transformation between these models, as well as to executable source code, for instance, for Lego robots will contribute to a complete hybrid systems modeling experience.

 

Employed Technologies: Eclipse, Java Eclipse Modelling Framework (EMF/GMF), XText, Transformation Languages, KeYmaera Verification Tool, Colored Petri Nets, Hybrid Petri Nets

 

Open Topics for Seminar/Bachelor's/Master's Projects

  • Topic 1: A Textual Eclipse-based Editor for (Distributed) Differential Dynamic Logic
  • Topic 2: Transformations between Models of Differential Dynamic Logic and Distributed Differential Dynamic Logic
  • Topic 3: Hybrid Program Model Templates and their Automated Verification in KeYmaera and KeYmaeraD
  • Topic 4: Transformation of Hybrid Programs to Hybrid Petri Nets for Liveness Verification Purposes
  • Topic 5: Simulation of Hybrid Programs in NetLogo
  • Topic 6: A Debugger for Hybrid Programs
  • Topic 7: Transformation of Hybrid Programs to robot control code (e.g., Lego Mindstorms)
  • Topic 8: Comparison, Versioning, and Graphical Analysis of Proof Trees
  • Topic 9: Formal Verification of Real-World Cyber-Physical Systems (selection of road traffic control, robot navigation, or any other topic of interest)

Current Projects

  • Conceptualization, Design, and Automated Testing of an Eclipse-based Modeling Environment (Ralph Mayr)

Finished Projects

  • Modeling and Verification of Continuous Object Behavior and Discrete Control Actions in Situation Awareness Systems (Stefan Mitsch)