Modular Design of Hybrid Systems

Project description

The approach concentrates on the formal development of real-life hybrid technical systems. A specification technique for the formal design, analysis, and verification of continuous-discrete models is developed which, particularly, facilitates the modular development of distributed process control software. It is based on the approach TLA (Temporal Logic of Actions) by Leslie Lamport. Extensions of TLA with regard to modularization as well as to the specification of real-time and hybrid systems are developed. The project concentrates mainly on practical topics: specification language, application methods, libraries of specification patterns (particularly for the control of chemical processes), and tools. It provides a framework facilitating the formal specification of hybrid technical systems and the hazard analysis by formal logical verification.

Publications

P. Herrmann, H. Krumm, O. Drögehorn, W. Geisselhardt: Framework and Tool Support for Formal Verification of High Speed Transfer Protocol Designs.
In: Telecommunication Systems, Kluwer Academic Publisher, 20(2002)3-4, 291-310.

S. Kowalewski, P. Herrmann, S. Engell, R. Huuck, H. Krumm, Y. Lakhnech, B. Lukoschus, H. Treseler: Approaches to the Formal Verification of Hybrid Systems.
In: at - Automatisierungstechnik, 49(2001)2, 66-74.

P. Herrmann, H. Krumm: A Framework for the Hazard Analysis of Chemical Plants.
In: Proceedings of the 11th IEEE International Symposium on Computer-Aided Control System Design (CACSD2000), pages 35-41, Anchorage, Alaska, USA, IEEE CSS, September 2000. Omnipress.

P. Herrmann, P. Grannas: A Tool for Hazard Detection in Hybrid Systems.
In: Proceedings of the 4th International Conference on Automation of Mixed Processes: Hybrid Dynamic Systems, pages 225-230, Dortmund, Germany, September 2000. Shaker Verlag.

P. Herrmann, M. Noël: Formal Development of a Distributed Control System for Road Marking Machines.
In: 8th International Conference on Telecommunication Systems - Modelling and Analysis, pages 430-437, ATSMA, IFIP, Nashville, TN, USA, 2000.

P. Herrmann, H. Krumm: Formal Hazard Analysis of Hybrid Systems in cTLA.
In: 18th IEEE Symposium on Reliable Distributed Systems (SRDS´99), pages 68-77, Lausanne, Oct. 1999, IEEE Computer Society Press.

P. Herrmann, M. Noël: Formale Verifikation eines Reglers für Fahrbahnmarkierungsmaschinen.
In: Tagungsband zum 9. Fachgespräch Formale Beschreibungstechniken, Seiten 83-92, München, HerbertUtz-Verlag, 1999. (In German)

P. Herrmann, O. Drögehorn, W. Geisselhardt, H. Krumm: Tool-supported formal verification of highspeed transfer protocol designs.
In: 7th International Conference on Telecommunication Systems - Modelling and Analysis, pages 531-541, ATSMA, IFIP, Nashville, TN, USA, 1999.

P. Herrmann, G. Graw, H. Krumm: Compositional Specification and Structured Verification of Hybrid Systems in cTLA.
In: Proceedings of the 1st IEEE International Symposium on Object-oriented Real-time distributed Computing - (ISORC'98), pages 335-340, Kyoto, Japan, 1998, IEEE Computer Society Press.

P. Herrmann, H. Krumm: Specification of Hybrid Systems in cTLA+.
In: Proceedings of the 5th International Workshop on Parallel & Distributed Real-Time Systems - (WPDRTS'97), pages 212-216, IEEE, Geneva, Switzerland, 1997, IEEE Computer Society Press.

P. Herrmann, H. Krumm: Kompositionale Constraints hybrider Systeme.
In: Tagungsband zur 5. Fachtagung Entwurf komplexer Automatisierungssysteme, pages 243-264,
Braunschweig, Mai 1997. In German.

P. Herrmann, H. Krumm: Compositional Specification and Verification of High-Speed Transfer Protocols.

In: S. T. Vuong and S. T. Chanson, editors, Protocol Specification, Testing and Verification XIV, pages 339-346, Vancouver, B.C., Canada, 1994. Chapman and Hall.

Project Results

Framework for the Hazard Analysis of Hybrid Technical Systems

Project Partner

Deutsche Forschungsgemeinschaft (DFG)
Programme: Analysis and Synthesis of Continuous-Discrete Technical Systems (KONDISK)

Project Duration

March 1996 - February 1999

Contact

Peter Herrmann

Peter Herrmann, February 22, 2001
Informatik IV, Uni Dortmund