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.