Approaches to the Formal Verification of Hybrid Systems

Stefan Kowalewski

Address: Robert Bosch GmbH, FV/SLD, Postfach 90 01 69, D-60441 Frankfurt am Main, Germany
E-Mail: stefan.kowalewski@de.bosch.com

Peter Herrmann

Address: Universität Dortmund, FB Informatik, LS IV, D-44221 Dortmund, Germany
E-Mail: Peter.Herrmann@cs.tu-dortmund.de

Sebastian Engell

Address: Universität Dortmund, FB Chemietechnik, LS AST, D-44221 Dortmund, Germany
E-Mail: s.engell@ct.tu-dortmund.de

Ralf Huuck

Address: Christian-Albrechts-Universität Kiel, Institut für Informatik und Praktische Mathematik, Preußerstraße 1-9, D-24105 Kiel, Germany
E-Mail: rhu@informatik.uni-kiel.de

Heiko Krumm

Address: see Peter Herrmann
E-Mail: krumm@cs.tu-dortmund.de

Yassine Lakhnech

Address: Laboratoire VERIMAG, Centre Equation, 2 av. de Vignate, F-38160 Gières, France
E-Mail: yassine.lakhnech@imag.fr

Ben Lokoschus

Address: see Ralf Huuck
E-Mail: bls@informatik.uni-kiel.de

Heinz Treseler

see Sebastian Engell
E-Mail: h.treseler@ct.tu-dortmund.de

Abstract

This paper presents two different approaches to the problem of formally verifying the correctness of control systems which consist of a logic controller and a continuous plant and, thus, constitute a hybrid system. One approach aims at algorithmic verification and combines Condition/Event Systems with Timed Automata. The first framework is used to model the controller and the plant in a block-diagram representation, which is then translated into the latter model for analysis by available tools. A second approach is presented which is based on deductive verification. It allows for a structured analysis of compositional specifications formulated in a temporal logic called cTLA. This logic is a compositional style of the Temporal Logic of Actions established in Computer Science by Lamport. Both approaches are introduced using a common example and the results of their application are discussed. As an outlook, a possible strategy for integrating algorithmic and deductive verification of hybrid systems is sketched at the end of the paper.

Published in

at - Automatisierungstechnik, Special Issue Hybrid Systems II: Analysis, Modeling, and Verification, 49(2001)2, 66-74, Oldenbourg Verlag.

Obtaining the paper

Due to the copyright agreement between the publisher and the authors we are not allowed to make the paper available online. If you have problems to obtain it, please call us.