Ara*_*raK 12 language-agnostic logic formal-verification
我在大学里瞥见了Hoare Logic.我们做的很简单.我所做的大部分工作都证明了由while循环,if语句和指令序列组成的简单程序的正确性,但仅此而已.这些方法似乎非常有用!
工业上使用的正式方法是否广泛？
这些方法是否用于证明任务关键型软件？
Jör*_*tag 14
好吧,Tony Hoare爵士大约10年前加入了微软研究院,他开始的事情之一就是对Windows NT内核的正式验证.实际上,这是Windows Vista长时间延迟的原因之一:从Vista开始,内核的大部分内容实际上已经过正式验证.某些属性,如没有死锁,没有信息泄漏等.
这当然不是典型的,但它可能是正式程序验证的唯一最重要的应用,就其影响而言(毕竟,几乎每个人都以某种方式,形状或形式受到运行Windows的计算机的影响).
Ada*_*ght 12
这是一个让我心动的问题(我是使用正式逻辑进行软件验证的研究员),所以当我说我认为这些技术有用的地方,并且还没有充分使用时,你可能不会感到惊讶.行业.
有很多级别的"形式方法",所以我假设你的意思是那些在严格的数学基础上休息的人(而不是说,遵循一些6-Sigma风格的过程).某些类型的形式方法取得了巨大成功 - 类型系统就是一个例子.基于数据流分析的静态分析工具也很受欢迎,模型检查在硬件设计中几乎无处不在,而像Pi-Calculus和CCS这样的计算模型似乎激发了实用语言设计中并发性的一些真正变化.终止分析最近有很多新闻报道 - 微软的SDV项目和Byron Cook的工作是最近在正式方法中进行研究/实践交叉的例子.
到目前为止,Hoare Reasoning还没有在行业中取得很大的进展 - 这比我列出的更多的原因,但我怀疑主要是围绕编写的复杂性,然后证明真正的程序规范(他们往往变大,失败)表达许多现实世界环境的属性).这种推理中的各种子领域现在正在大力解决这些问题 - 分离逻辑就是其中之一.
这部分是正在进行的(硬)研究的本质.但我必须承认,作为理论家,我们完全没有教育行业为什么我们的技术有用,使它们与行业需求相关,并使它们与软件开发人员平易近人.在某种程度上,这不是我们的问题 - 我们是研究人员,通常是数学家,实际使用并不是我们的首要考虑因素.此外,正在开发的技术通常过于萌芽,无法在大规模系统中使用 - 我们在小型程序上工作,在简化系统上工作,使数学工作,并继续前进.我不太喜欢这些借口 - 我们应该更积极地推动我们的想法,并在行业和我们的工作之间获得反馈循环(我回到研究的主要原因之一).
对我来说,复活我的博客可能是一个好主意,并在这些东西上发表更多帖子......
虽然我知道航空电子行业使用各种各样的技术来验证软件,包括Hoare风格的方法,但我对关键任务软件的评论不多.
正式的方法受到了影响,因为像Edsger Dijkstra这样的早期倡导者坚持认为它们应该在任何地方使用.形式主义和软件支持都不能胜任这项工作.更明智的倡导者认为,这些方法应该用于难以解决的问题.它们并未在工业中广泛使用,但采用率正在提高.可能最大的进展是使用正式方法来检查软件的安全属性.我最喜欢的一些例子是SPIN模型检查器和George Necula的携带证明的代码.
从实践到研究,Microsoft的Singularity操作系统项目是使用正式方法提供通常需要硬件支持的安全保证.这反过来又会带来更快的性能和更强的保证.例如,在奇点中他们已经证明,如果允许第三方设备驱动程序进入系统(这意味着已经证明基本验证条件),那么它不可能降低整个操作系统 - 它最糟糕的是它可以做到自己的设备.
正式方法尚未在工业中广泛使用,但它们的使用比20年前更广泛,20年后它们将被更广泛地使用.所以你有前瞻性:-)
是的,它们被使用,但在所有领域都没有广泛使用.除了hoare逻辑之外,还有更多的方法,有些被更多地使用,有些则更少,这取决于给定任务的适用性.常见的问题是,软件是biiiiiiig并且验证所有这些都是正确的仍然是一个太难的问题.
例如,定理证明器(帮助人类证明程序正确性的软件)ACL2已被用于证明某个浮点处理单元没有某种类型的错误.这是一项艰巨的任务,所以这种技术并不常见.
模型检查是另一种形式验证,现在使用相当广泛,例如Microsoft在驱动程序开发工具包中提供了一种模型检查器,它可用于验证驱动程序是否存在一组常见错误.模型检查器也经常用于验证硬件电路.
严格的测试也可以被认为是形式验证 - 有一些正式的规范,应该测试哪些程序路径等等.