问题标签 [formal-verification]

• 您将模型检查用于哪些类型的应用程序？
• 你用的是什么模型检查工具？
• 您如何总结您使用该技术的经验，特别是在评估其交付更高质量软件的有效性方面？

在我的学习过程中，我有机会使用Spin，它引起了我的好奇心，即实际进行了多少模型检查以及组织从中获得了多少价值。在我的工作经验中，我从事过业务应用程序，其中（自然）没有考虑将形式验证应用于逻辑。我真的很想了解 SO 人的模型检查经验和对该主题的想法。模型检查会成为我们应该在我们的工具包中使用的更广泛使用的开发实践吗？

为什么不能像数学陈述一样证明计算机程序？数学证明建立在其他证明的基础上，这些证明建立在更多证明和公理之上——我们认为这些真理是不言而喻的。

计算机程序似乎没有这样的结构。如果你写一个计算机程序，你怎么能把以前证明过的作品拿来用它们来证明你的程序的真实性？你不能，因为不存在。此外，编程的公理是什么？该领域的原子真理？

我对上述问题没有很好的答案。但似乎软件无法被证明，因为它是艺术而不是科学。如何证明毕加索？

我一直在做一个项目，它是一个应用服务器和一个对象数据库的组合，目前只在一台机器上运行。前段时间，我阅读了一篇描述分布式关系数据库的论文，并获得了一些关于如何将论文中的想法应用到我的项目中的想法，这样我就可以使用共享的集群创建一个运行在集群上的高可用性版本- 无架构。

我的问题是，我没有设计分布式系统及其协议的经验——我没有在大学学习关于分布式系统的高级 CS 课程。所以我很担心能不能设计出一个不会造成死锁、饥饿、脑裂等问题的协议。

问题：我在哪里可以找到关于设计分布式系统的好资料？有哪些方法可以验证分布式协议是否正常工作？欢迎推荐书籍、学术文章等。

我们的客户希望我们构建一个基于 Web 的富 Internet 应用程序来收集软件需求。基本上，它是一个基于 Web 的案例工具，遵循特定流程从利益相关者那里获取需求。我是项目经理，我们仍处于项目的早期阶段。

我一直在考虑使用形式化方法来帮助我的客户和开发人员澄清对工具的要求。我所说的形式方法是指某种形式的建模，可能是基于数学的。我已经阅读并正在考虑的一些内容包括 Z ( http://en.wikipedia.org/wiki/Z_notation )、状态机、UML 2.0（可能带有OCL等扩展）、Petri 网和一些编码合同和前置条件和后置条件等级别的东西。还有什么我应该考虑的吗？

开发人员经验丰富，但根据所使用的形式，他们可能需要学习一些数学知识。

我正在尝试确定我是否值得在这个项目上使用形式化方法，如果是，在多大程度上。我知道“这取决于”，所以对我来说最有帮助的答案是是/否和支持论点。

如果你在这个项目中，你会使用正式的方法吗？

我想知道如何\old(Expression[Id])评估表单的 JML 表达式，即如果我有\old(vector[value-1])表达式，是否\old也指“值”或仅指vector[value-1]. 提前致谢！

我在大学时瞥见了Hoare Logic。我们所做的非常简单。我所做的大部分工作是证明由while循环、if语句和指令序列组成的简单程序的正确性，但仅此而已。这些方法看起来很有用！

形式化方法是否在工业中广泛使用？

这些方法是否用于证明关键任务软件？

我是一名对信息检索感兴趣的软件开发人员。目前我正在处理我的第三个搜索引擎项目，并且对一次又一次编写的样板代码数量感到非常沮丧，同样的错误等等。

基本搜索引擎是一个非常简单的野兽，可以用由两个“层”组成的正式语言来描述：

1. “原语层”（或公理，内核语言 - 不知道如何命名它们）。它们包括几个集合（作为一组资源 - 文件、网站）、集合上的关系（作为“站点 A 链接到站点 B”）和简单的操作，例如“打开资源 A 的流”、“从流中读取记录”、 'merge N 个流'，'index set of records by field F'等。还有很多数据转换，如'save stream in YAML format'，'load stream from XML format'等。

2. “应用层”——构成搜索引擎生命周期的几个非常高级的操作，如“收获新资源”、“抓取收获的资源”、“将抓取的资源合并到数据库”、“索引抓取的资源”、“合并索引”等等。每一个高级操作都可以用从 1 开始的“原语”来表示。

这种高级表示可以很容易地测试，甚至可以正式证明，并用所选的编程语言实现（或代码生成）。

那么问题来了：是否有人以这种方式设计系统——形式上、严格（甚至可能在代数/群论的层面上），在严格的自上而下的方法中？我可以阅读以了解什么？

首先，这是否仅适用于没有副作用的算法？

其次，我在哪里可以了解这个过程，有什么好书、文章等？

我有一个宏伟的想法，即基本上采用一些蛮力攻击来测试/验证我的 Web 应用程序不会崩溃。

不要让我开始单元测试和 IoC 的东西，这完全是另一回事。

我正在做的，以及我正在寻求帮助的是创建一个智能详尽的搜索，探索程序状态的一部分。

我所拥有的是一个网页，其中包含我可以做的事情，单击是一回事，文本输入是另一回事，一些输入（如单选按钮和下拉列表）被限制为某些值。很基本的东西。我最终得到一组有限的事件和值，而我想要建模的是状态的进展。也许这在某种程度上是 FSM 优化，但目标是系统地检查事件和值的任意排列，看看会发生什么。

当发现问题时，我想尝试以尽可能少的努力引发该错误，以便能够呈现清晰的测试用例。

这与形式验证方法有关，我正在向有经验的人寻求帮助或见解。

我希望能够将大测试拆分为较小的测试，以便当较小的测试通过时，它们暗示大测试也会通过（因此没有理由运行原始的大测试）。我想这样做是因为较小的测试通常需要更少的时间、更少的精力并且更不脆弱。我想知道是否有测试设计模式或验证工具可以帮助我以稳健的方式实现这种测试拆分。

我担心当有人更改较小测试集中的某些内容时，较小测试和原始测试之间的联系会丢失。另一个担心是较小的测试集并没有真正涵盖大的测试。

我的目标是一个例子：