Conference Paper (in Formal Publication) ()
Wilson T, Maharaj S & Clark R (2005) Omnibus verification policies: A flexible, configurable approach to assertion-based software verification In: Aichernig BK, Beckert B (ed.) SEFM 2005: Third IEEE International Conference on Software Engineering and Formal Methods, Proceedings, Los Alamitos, CA: The Institute of Electrical and Electronics Engineers, Inc. 3rd IEEE International Conference on Software Engineering and Formal Methods, 7.9.2005 - 9.9.2005, Koblenz, Germany, pp. 150-159.
The three main assertion-based verification approachesare: Design by Contract (DBC), Extended Static Checking(ESC) and Verified Design by Contract (VDBC). Each approachoffers a different balance between rigour and easeof use making them appropriate in different situations. Ourgoal is to explore the use of these approaches together in aflexible way, enabling an application to be broken downinto sections with different reliability requirements and differentverification approaches used in each section. We explainthe benefits of using the approaches together, presenta set of guidelines to avoid potential conflicts and give anoverview of how the Omnibus IDE provides support for thefull range of assertion-based verification approaches withina single tool.
formal methods; software verification; design by contract; static checking
|Editor||Aichernig BK, Beckert B|
|Authors||Wilson Thomas, Maharaj Savi, Clark Robert|
|Publisher||The Institute of Electrical and Electronics Engineers, Inc|
|Place of publication||Los Alamitos, CA|
Sefm 2005: Third Ieee International Conference on Software Engineering and Formal Methods, Proceedings (2005)