SearchPublisher and Institutes
You are here: Home :: Area NEM :: Engineering :: Automation
Stefan Kowalewski, P. Herrmann, Sebastian Engell, R. Huuck, H. Krumm, Y. Lakhnech, B. Lukoschus, H. Treseler
Approaches to the Formal Verification of Hybrid Systems
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.
at – Automatisierungstechnik, Oldenbourg Wissenschaftsverlag
Print ISSN: 0178-2312
Volume: 49, 02/2001
Pages: 66