Skip header navigation
×

Conference Proceeding

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

StatusPublished
Author(s)Wilson, Thomas; Maharaj, Savi; Clark, Robert
Publication date31/12/2005
URLhttp://hdl.handle.net/1893/10325
PublisherThe Institute of Electrical and Electronics Engineers, Inc
Publisher URLhttp://ieeexplore.ieee.org/…p?punumber=10529
Place of publicationLos Alamitos, CA
ISBN0-7695-2435-4
Conference3rd IEEE International Conference on Software Engineering and Formal Methods
Conference locationKoblenz, Germany
Dates
Scroll back to the top