正式的程序验证方法是否在行业中占有一席之地？
https://stackoverflow.com/questions/1196803
-
20-09-2019 - |
italiano
english
français
española
中国
日本の
العربية
Deutsch
한국어
Português
Russian题
我瞥见了 Hoare逻辑 在大学。我们所做的真的很简单。我所做的大部分是证明了简单程序的正确性，包括 while 循环， if 陈述和指示顺序，但仅此而已。这些方法似乎非常有用！
行业中使用形式方法吗？
这些方法是否用于证明关键任务软件？
解决方案
这是一个靠近我心的问题（我是使用正式逻辑的软件验证研究人员），因此，当我说这些技术有一个有用的地方，并且在该公司中尚未使用时，您可能不会感到惊讶行业。
有很多级别的“形式方法”，所以我假设您的意思是那些基于严格的数学基础（而不是按照6个sigma样式的过程）。某些类型的形式方法取得了巨大的成功 - 类型系统就是一个例子。基于数据流量分析的静态分析工具也很受欢迎，模型检查在硬件设计中几乎无处不在，而Pi-Calculus和CC等计算模型似乎在启发了实用语言设计的真正变化以进行并发。终止分析是最近有很多媒体的分析-Microsoft的SDV项目，拜伦·库克（Byron Cook）的工作是正式方法中研究/实践交叉的最新示例。
到目前为止 大的, ，并且无法表达许多现实世界环境的属性）。现在，这种推理中的各种子场正在涉足这些问题 - 分离逻辑是一个。
这部分是正在进行的（艰苦）研究的本质。但是，我必须承认，作为理论家，我们完全未能教育行业有关我们的技术为何有用的，以使其与行业需求保持相关，并使它们对软件开发人员的平易近人。在某种程度上，这不是我们的问题 - 我们是研究人员，通常是数学家，实际用途并不是我们的思想。同样，开发的技术通常太胚胎了，无法在大规模系统中使用 - 我们从事小程序，简化系统，进行数学工作并继续前进。不过，我不多买这些借口 - 我们应该更积极地推动我们的想法，并在行业和我们的工作之间获得反馈循环（我重返研究的主要原因之一）。
对我来说，复活我的博客并在这些东西上发表更多帖子可能是个好主意...
其他提示
好吧，托尼·霍尔爵士（Tony Hoare）爵士大约在10年前加入了微软的研究，他开始的一件事是对Windows NT内核的正式验证。的确，这是Windows Vista长时间延迟的原因之一：从Vista开始，内核的大部分 是 实际经过正式验证的WRT。对于某些特性，例如没有僵局，没有信息泄漏等。
这当然不是典型的，但是就其影响而言，它可能是正式程序验证的最重要应用（毕竟，几乎每个人都以某种方式，形状或形式受到计算机运行窗口的影响）。
我对关键任务软件的评论不能太多，尽管我知道航空电子行业使用多种技术来验证软件，包括Hoare风格的方法。
正式的方法之所以受苦，是因为像埃德斯·迪克斯特拉（Edsger Dijkstra）这样的早期拥护者坚持认为，他们应该在任何地方使用。形式主义和软件支持都不取决于工作。更明智的拥护者认为，这些方法应用于困难的问题。它们并不广泛用于行业，但采用率正在增加。可能最大的进攻是使用正式方法来检查 安全性能 软件。我最喜欢的一些例子是 旋转 模型检查器和乔治·尼库拉（George Necula）的证明代码。
从实践中移开研究，微软的 奇异性 操作系统项目旨在使用正式方法来提供安全保证，即通常需要硬件支持。反过来，这会导致更快的性能和更强的保证。例如，以奇异性证明，如果允许第三方设备驱动程序进入系统（这意味着已经证明了基本验证条件），那么它不可能放下整个OS，他可以做的最糟糕的是它是软管自己的设备。
正式方法尚未在行业中广泛使用，但与20年前相比，它们更广泛地使用，从现在起20年后，它们将被更广泛地使用。因此，您是未来的:-)
是的，它们被使用，但在所有领域都没有广泛使用。除了hoare逻辑外，还有更多的方法，有些使用更多，有些使用，具体取决于适合给定任务的方法。常见的问题是，Sofware是Biiiiiiig，并验证所有这些都是正确的仍然是一个难题。
例如，定理 - 示威者（一种有助于人类证明程序正确性的软件）ACL2已被用来证明某个浮点处理单元没有某种类型的错误。这是一项艰巨的任务，因此这种技术并不常见。
如今，模型检查是另一种正式验证，例如，Microsoft在驱动程序开发套件中提供了一种模型检查器，可用于验证一组常见错误的驱动程序。模型检查器也经常用于验证硬件电路。
严格的测试也可以被认为是正式验证 - 有一些正式的规范应测试程序的路径等。
“行业中使用形式的方法吗？”
是的。
这 assert 许多编程语言的语句与用于验证程序的形式方法有关。
“行业中使用正式方法吗？”
不。
“这些方法是否用于证明关键任务软件？”
有时。通常，它们用来证明该软件是安全的。更正式地，它们用于证明有关该软件的某些与安全有关的断言。
行业中有两种不同的方法。
一种方法是完全改变开发过程。提到的Z符号和B方法是在第一类中。 B被应用于巴黎的无人驾驶地铁线14（如果有机会，请爬上前货车。
另一种更加增量的方法是保留现有的开发和验证过程，并一次仅通过一种新方法替换一个验证任务之一。这非常有吸引力，但这意味着开发静态分析工具，用于退出，使用通常不容易分析的语言（因为它们不是为其设计的）。如果您去（例如）
http://dblp.uni-trier.de/db/indices/a-tree/d/delmas:david.html
（抱歉，新用户只允许一个超链接:(）
您会发现正式方法在C验证C程序的实例（使用静态分析师Astrée，Caveat，Folluctuat，Frama-C）和二进制代码（带有Absint GmbH的工具）。
顺便说一句，由于您在上述工具列表中提到了hoare逻辑，因此只有警告是基于hoare逻辑（并且frama-c具有HOARE逻辑插件）。其他人则依靠抽象解释，这是一种采用更自动方法的不同技术。
我的专业知识领域是将正式方法用于静态代码分析，以表明软件没有运行时错误。这是使用已知“抽象解释”的形式方法来实施的。该技术实质上使您能够证明AS/W程序的某些侵犯。例如，证明A+B不会溢出或X/（XY）不会导致除以零。使用此技术的示例静态分析工具是polyspace。
关于您的问题： “行业中使用正式方法吗？” 和 “这些方法是否用于证明关键任务软件？”
答案是肯定的。该意见是基于我的经验和支持用于控制安全关键系统的行业的Polyspace工具，例如在汽车中的电子油门等安全系统，用于火车，喷气发动机控制器，药物输送泵，药物输送泵，制动系统，等等。这些行业确实确实使用了这些类型的形式方法工具。
我不认为这些行业中的所有100％都在使用这些工具，但是使用量正在增加。我认为，航空航天和汽车行业领导着医疗设备行业迅速增加使用。
Polyspace 是基于程序验证的AA（非常昂贵但非常好的）商业产品。这是相当务实的，因为它可以从“增强的单元测试可能会发现一些错误”到“生命的未来三年”将显示这10个文件的缺陷为零。
它更多地基于负面验证（“此程序不会损坏您的堆栈”），而不是正面验证（“该程序将确切地完成这50页的方程式所说的内容”）。
除了其他更多程序性方法外，Hoare逻辑还基于 通过合同设计, ，由贝特兰·迈耶（Bertrand Meyer）在埃菲尔（Eiffel参见迈耶（Meyer）的1992年文章, ，第4页）。虽然合同设计与正式验证方法不同（一方面，DBC没有 证明 在执行软件之前的任何内容），我认为它提供了更实际的用途。
