“程序测试能证明错误的存在,但不能证明错误不存在”。Edsger Dijkstra(1972年图灵奖获得者、形式化方法核心思想的提出者)如此评述。
在实践中,尤其是在代码足够复杂的场景中,形式化验证(Verification)与程序测试方法(Testing) 的验证效果有如云泥之别。
举个例子来说:2009年,澳大利亚的科学家使用形式化方法对工业级操作系统seL4微内核进行了完整功能性验证,验证方式同时以形式化验证和程序测试两种方式分别展开,验证的结果是:形式化方法共发现460多个Bug,而程序测试只发现了16个Bug。更有趣的是,在以高验证成本著称的形式化验证领域,完全验证seL4微内核只需要600万美元的验证成本,而以测试的方式通过CC EAL6级认证的成本竟高达8700万美元。
由此可见,通过形式化验证可以更经济的为seL4微内核提供更强的安全性保证。
国际第一个并发C程序完全形式验证工具
国内第一个支持高级别安全认证的形式开发框架
国际第一个多核/可中断系统组合验证工具
咨询热线:18358509111 运营中心:400-675-8118
E-mail:wangan@wonsec.com 邮政编码:312000
地址:浙江省绍兴市柯桥区齐贤街道柯桥经济技术开发区西环路586号科创大厦A座507-508
版权所有 Copyright ©2019-2020 浙江望安科技有限公司 网络备案号:浙ICP备19042838号-1