Pascal Montag, Dirk Nowotka, and Paul Levi
Verification in the Design Process of Large Real-Time Systems: A Case Study


In E. Plödereder, H. B. Keller, P. Dencker, and M. Tonndorf (eds), Automotive - Safety & Security 2006 - Sicherheit und Zuverlässigkeit für automobile Informationstechnik, Stuttgart, Shaker Verlag, Aachen, 2006.

Abstract

A verification case study of a complex real-time system from the automotive area, an emergency brake assistant, is conducted. In particular the application and usefulness of formal methods in the refinement process during the design of a large system is investigated, where we mean by "large system" a system which cannot be formally verified as a whole due to its complexity. We establish that the application of formal methods in the early phase of a system design is beneficial despite the limits of current tools. Useful directions of further work to improve the verified design of safety-critical systems are also shown.

Keywords: real-time systems, verification, design process

Full paper: [pdf - 423 KB].