University of Stirling@milan米兰体育 灵活且可配置的综合验证政策

引用

Wilson T、Maharaj S 和 Clark R (2008) 使用 Omnibus 实现灵活且可配置的验证策略。软件和系统建模，7 (3)，第 257-272 页。 http://www.springerlink.com/content/9543347t1h403181/fulltext.pdf； https://doi.org/10.1007/s10270-007-0060-1

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

关键字
;计算机程序验证；综合（计算机程序语言）

期刊
软件和系统建模：第 7 卷，第 3 期

• 威尔逊马哈拉杰克拉克.pdf