FB3
TZI
BISS
HYBRIS: Efficient Analysis of Hybrid Systems (1999 - 2005)
This project is a sub-project in a DFG-funded priority programme Integration of Software Specification Techniques for Scientific Engineering Applications SPP 1064
Project Leaders
Jan Peleska and B.-H. Schlingloff (1999 - 2001)Researchers funded by DFG
Stefan BisanzContact
Jan PeleskaProject Description
This project integrates description techniques widely used in the engineering sciences (timing diagrams and differential equations) with formal specification techniques that have been mostly used in the computer science communities. The integrated application of these techniques is demonstrated by means of case studies from the field of railway control systems. Furthermore, it was investigated whether concepts based on partial-order theories can be applied in the context of these specification techniques. The motivation for this integration approach is as follows: The engineering sciences provide a substantial knowledge about control theory based on (systems of) differential equations. However, today´s computerised applications in this field require to implement the control-theoretic model by embedding it into a software system and its underlying hardware consisting of controllers, digital interfaces, sensors and actuators. As a consequence, it is necessary to provide an integrated technique for the specification, verification, validation and test of both the control-theoretic and the software-related aspects of the system. To achieve this, we start by investigating a semantic framework based on timed transition systems enhanced by systems of differential equations. This will lead to a ``generic procedure'' describing how control-theoretic aspects can be soundly integrated into any formal specification technique based on this semantic framework. To make large hybrid system specifications manageable, we will investigate a structural decomposition technique transforming the original specification into a collection of cooperating sub-specifications. Each sub-specification is an instance of a class of generic specifications possessing a restricted structure which is easier to handle than an arbitrary admissible hybrid specification structures. In addition to the formal specification and verification, it will be possible to derive tests from hybrid specifications and evaluate test executions automatically against the specified system behaviour. To reduce the number of execution sequences possible in a general hybrid system, partial-order modelling techniques are investigated to separate relevant causal relations which have to be tested and therefore should lead to specific execution sequences from unrelated events where any order in the test execution is admissible.Most Recent Project Results
The results achieved in the final project phase are available as- Final project report (in German) and
comprehensive list of publications
- HYBRIS Part I: HybridUML - a UML 2.0 profile for the specification of
Hybrid Systems
HybridUML (last updated on 2006-04-13).
- HYBRIS Part II: HL3 - a formal real-time specification language framework
serving as compilation target for various high-level specification formalisms,
such as HybridUML specifications. HL3 low-level specifications can be compiled
into programs executable in hard real-time on multi CPU cluster PC architectures.
The Hybrid Low-Level Language Framework HL3
(last updated on 2006-04-27).
- HYBRIS Part III: RCSD - a UML 2.0 profile for the Railway Control System
Domain
RCSD (last updated on 2006-12-18).
- HYBRIS Part IV: An approach to model-based Hybrid Systems Testing --
see full versions of the papers
- Bahareh Badban, Martin Fränzle, Jan Peleska and Tino Teige: ¨ Test Automation for Hybrid Systems (Accepted in shortened form for publication in proceedings of the SOQUA2006, last updated on 2006-10-08)
- Martin Fränzle, Jan Peleska and Tino Teige: ¨
Symbolic Test Case Generation for Time-Discrete Hybrid Systems
(submitted to RTAS 2006, last updated on 2006-10-19)
- HYBRIS Part V: Specification and Verification of Railway Control Systems (to
appear)
- The following dissertation theses were accomplished within the HYBRIS project:
- Stefan Bisanz: Executable HybridUML. A Transformation Definition.
- Markus Dahlweid, Uwe Schulze: High Level Transition Systems of CSP Specifications and their Application in Automated Testing
- Detlef Kendelbacher: Architekturkonzept und Designaspekte einer signaltechnisch nichtsicheren Kommunikationsplattform für sicherheitsrelevante Bahnanwendungen.
- Oliver Meyer: Structural Decomposition of Timed CSP and its Application in Real-Time Testing.
- Peter Amthor: Structural Decomposition of Hybrid Systems Test Automation for Hybrid Reactive Systems.
- The following habilitation theses were accomplished within the HYBRIS
project:
- Holger Schlingloff: Partial State Space Analysis of Safety-Critical Systems
- Bettina Buth: Formal and Semi-Formal Methods for the Analysis of Industrial Control Systems.
- Jan Predereke: Maintaining Families of Rigorous Requirements for Embedded Software Systems.
- The following links refer to publication lists of authors who contributed
to the HYBRIS project.
- Publications of Jan Peleska
- Publications of Holger Schlingloff
- Publications of Jan Bredereke
- Publications of Kirsten Berkenkötter
- Publications of Stefan Bisanz
- Publications of Ulrich Hannemann
Case Studies
The case studies to be investigated in the HYBRIS project comprise-
Railway Traffic Control (Project Reference Case
Study)
- Dracos: Verification of a Distributed Railway Control System
Recent Presentations
Hybrid UML and its Application to Specification and Test of Train Control Systems. Part 2
presented at the "6. Kolloquium des DFG-SPP 1064 Software-Spezifikationen" in Stuttgart, Germany, 20.11.2003HYBRIS - Efficient Analysis of Hybrid Systems
presented at the "Abschlusskolloquium (7. Kolloquium) des DFG-SPP 1064 Software-Spezifikationen" in Stuttgart, Germany, 28.09.2004
Author: jp
| Last updated: November 2, 2022 |  |