Modelling and Verification using Linear Hybrid Automata -- a Case Study

Olaf Müller and Thomas Stauner

Mathematical and Computer Modelling of Dynamical Systems, 2000, vol. 6, issue 1, 71-89

Abstract: This paper discusses the use of hybrid automata to specify and verify embedded distributed systems, that consist of both discrete and continuous components. The basis of the evaluation is an automotive control system, which controls the height of an automobile by pneumatic suspension. It has been proposed by BMW AG as a case study taken from a current industrial development. Essential parts of the system have been modelled as hybrid automata and for appropiate ions several safety properties have been verified. The verification has been performed using HYTECH, a symbolic model checker for linear hybrid automata. The paper discusses the general appropiateness of hybrid automata to specify hybrid systems as well as advantages and drawbacks of the applied model-checking techniques.

Date: 2000
References: Add references at CitEc
Citations:

Downloads: (external link)
http://hdl.handle.net/10.1076/1387-3954(200003)6:1;1-Q;FT071 (text/html)
Access to full text is restricted to subscribers.

Related works:
This item may be available elsewhere in EconPapers: Search for items with the same title.

Export reference: BibTeX RIS (EndNote, ProCite, RefMan) HTML/Text

Persistent link: https://EconPapers.repec.org/RePEc:taf:nmcmxx:v:6:y:2000:i:1:p:71-89

Ordering information: This journal article can be ordered from
http://www.tandfonline.com/pricing/journal/NMCM20

DOI: 10.1076/1387-3954(200003)6:1;1-Q;FT071

Access Statistics for this article

Mathematical and Computer Modelling of Dynamical Systems is currently edited by I. Troch

More articles in Mathematical and Computer Modelling of Dynamical Systems from Taylor & Francis Journals
Bibliographic data for series maintained by Chris Longhurst ().