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

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.