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 it will be meant by 'large system' a system which cannot be formally verified as a whole due to its complexity. The authors 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.
Verification in the design process of large real-time systems: a case study
Verifizierungen innerhalb eines Entwurfprozesses für umfangreiche Echtzeitsysteme: eine Fallstudie
2006
13 Seiten, 7 Bilder, 24 Quellen
Conference paper
English
Specification and Automated Verification of Real-Time Behaviour - A Case Study
British Library Conference Proceedings | 1995
|ABS: A CASE tool for real time systems design
British Library Conference Proceedings | 2000
|Formal modeling and verification of real-time concurrent systems
Tema Archive | 2008
|