University of Stirling@milan米兰体育 基于断言的集成验证与 Omnibus 的案例研究

引用

威尔逊 T、Maharaj S 和克拉克 R (2009)基于断言的集成验证与 Omnibus 的案例研究。技术报告 CSM，176。milan米兰体育计算科学与数学系。

摘要
我们展示了 Omnibus 中图书馆系统的规范、实现和验证示例。该示例应用了三种验证方法（运行时断言检查、扩展静态检查和完整形式验证），我们比较了每种方法的易用性和错误覆盖率。然后，我们讨论如何在 Omnibus 中以集成方式一起使用这三种方法，解释这样做的好处，并展示 Omnibus IDE 如何支持集成。

关键字
静态检查；运行时检查；综合形式化方法；面向对象；形式化方法（计算机科学）；决策，计算机辅助

• 基于断言的集成验证案例研究.pdf