Verification in the Design Process of Large Real-Time Systems: A Case Study
Paul A. Levi, Pascal Montag, Dirk Nowotka · 2006
A verification case study of a complex real-time 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 is investigated, where we mean by large system a 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 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.