|
Application name:
Chassis Level Control System
Organisation:
Munich University of Technology and BMW AG
Method:
Hybrid Automata
Tools:
HyTech
Domain:
Automotive control systems
Period:
June 1996 - February 1997
Size:
0.5 man-years
Description:
This case study shows how hybrid automata and the hybrid model-checker HyTech can be applied to specify and verify a part of an automotive control system. Furthermore, an approximation technique for hybrid automata, linear phase-portrait approximation, is extended to the parallel composition of hybrid automata.
The examined system controls the height of an automobile by a pneumatic suspension system and has been proposed by BMW AG as a case study taken from a current industrial development. Starting with a specification of a part of the electronic height control system consisting of statecharts and block diagrams, a hybrid automata specification is developed. General ideas for the translation from statecharts and block diagrams to hybrid automata are outlined. The hybrid automata specification is abstracted and the extended approximation technique is applied to enable analysis with HyTech. Finally several important properties of the system are verified using the model-checker.
Conclusions:
Hybrid automata are a promising approach for the specification of hybrid systems, as they allow to specify discrete and continuous properties of a system within one framework. For larger case studies a hierarchy concept would be desirable. Furthermore, appropriate tool support is necessary for the use in practice.
HyTech offers the great opportunity to automatically analyze properties ranging into the field of control theory. At present, however, the applicability of HyTech suffers from arithmetic overflow during the model-checking procedure and from high memory requirements.
Publications:
"Specification and Verification of an Electronic
Height Control System using Hybrid Automata". Thomas Stauner. http://www4.informatik.tu-muenchen.de/~stauner/da.ps.gz,
Master thesis, Munich University of Technology, 1997.
"Using HyTech to verify an Automotive Control System". Thomas Stauner, Olaf
M?ller and Max Fuchs. In HART'97, Proc. of the 1st International Workshop on Hybrid and
Real-Time Systems, LNCS 1201, Springer-Verlag, 1997.
Contact:
| Name: | Thomas Stauner |
| Organisation: | Computer Science Department, Munich University of Technology |
| Address: | D-80290 Munchen |
| Country: | Germany |
| Phone number: | +49 (89) 28928325 |
| Fax: | +49 (89) 28928183 |
| E-mail: | stauner@informatik.tu-muenchen.de |
| Personal website: | http://www4.informatik.tu-muenchen.de/~stauner/ |
|
