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. AbstractA 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]. |