Omnibus verification policies: A flexible, configurable approach to assertion-based software verification

Citation

Wilson T, Maharaj S & Clark R (2005) Omnibus verification policies: A flexible, configurable approach to assertion-based software verification. In: Aichernig B & Beckert B (eds.) SEFM 2005: Third IEEE International Conference on Software Engineering and Formal Methods, Proceedings. 3rd IEEE International Conference on Software Engineering and Formal Methods, Koblenz, Germany, 07.09.2005-09.09.2005. Los Alamitos, CA: The Institute of Electrical and Electronics Engineers, Inc, pp. 150-159. http://ieeexplore.ieee.org/xpl/mostRecentIssue.jsp?punumber=10529

Abstract
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.

Keywords
formal methods; software verification; design by contract; static checking