University of Stirling@milan米兰体育 综合验证政策：一种灵活、可配置的基于断言的软件验证方法

引用

Wilson T、Maharaj S 和 Clark R (2005) 综合验证策略：一种灵活、可配置的基于断言的软件验证方法。载于：Aichernig B 和 Beckert B（编辑）SEFM 2005：第三届 IEEE 软件工程和形式化方法国际会议，会议记录。第三届 IEEE 软件工程和形式方法国际会议，德国科布伦茨，2005 年 9 月 7 日至 2005 年 9 月 9 日。加利福尼亚州洛斯阿拉米托斯：电气和电子工程师协会，第 150-159 页。 http://ieeexplore.ieee.org/xpl/mostRecentIssue.jsp?punumber=10529

摘要
三种主要的基于断言的验证方法是：按合同设计 (DBC)、扩展静态检查 (ESC) 和按合同验证设计 (VDBC)。每种方法都在严格性和易用性之间提供了不同的平衡，使其适用于不同的情况。我们的目标是以灵活的方式探索这些方法的使用，使应用程序能够分解为具有不同可靠性要求的部分，并在每个部分中使用不同的验证方法。我们解释了一起使用这些方法的好处，提出了一组避免潜在冲突的指南，并概述了 Omnibus IDE 如何在单个工具中为全方位基于断言的验证方法提供支持。

关键字
正式方法；软件验证；按合同设计；静态检查