我应该在我的软件项目中使用形式化方法吗？ [关闭]答案

【问题标题】：Should I use formal methods on my software project? [closed]我应该在我的软件项目中使用形式化方法吗？ [关闭]
【发布时间】：2009-04-09 19:32:22
【问题描述】：

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

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

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

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

如果你参与这个项目，你会使用形式化方法吗？

【问题讨论】：

标签： web-applications modeling requirements formal-methods formal-verification

【解决方案1】：

我一直在考虑使用形式化方法来帮助我的客户和开发人员阐明对工具的要求。

很少有开发人员有正式方法的经验。当我们将CADiZ 移植到Windows 时，我唯一一次看到接受过正式方法培训的客户是ZUG 的成员。

我所说的形式化方法是指某种形式的建模，可能是基于数学的。我已经阅读并正在考虑的一些内容包括 Z (http://en.wikipedia.org/wiki/Z_notation)、状态机、UML 2.0（可能带有 OCL 等扩展）、Petri 网，以及一些编码级别的东西，如合同和前后条件.还有什么我应该考虑的吗？

Z 是一种形式化方法，以集合论为基础，而 UML 是一种带有一些半形式化符号（状态机）标记的非正式符号。

一些技术客户，例如您希望使用软件需求工具找到的客户，对 UML 非常满意。

创建域的 Z 模型可能有价值，创建客户端和服务器（或 petri-net）之间消息传递的 pi 演算模型可能有价值，但我发现 pi 既简单又强大）。

您的领域的 Z 模型将提供一组独立于实现的类型约束，其表达方式比任何常见实现语言的类型系统都更强大。

消息传递的正式模型将为您提供运行分析的便利，以确保您不会丢失更新或发生冲突或死锁。

UML 模型为您提供了一种符号，用于将大型系统分解为功能区域（包图），显示这些区域中的类如何静态地相互关联（类图），显示这些类的实例如何动态关联（序列图、活动图和交互图），并显示包的部署方式（组件和部署图）。这些对于团队中的沟通很有用，并且可以使想法更加充实，但没有正式定义的语义可以进行非常复杂的分析。

90 年代与我共事的 Z 专家认为在 Z 中指定 CASE GUI 的想法很荒谬。为这样的 GUI 创建 UML 模型很常见。

我没有使用正式的按合同设计的前置和后置条件，尽管我有时会在 cmets 中添加它们，并且经常在断言中添加它们，并且我对可能违反它们的条件进行单元测试。

【讨论】：

虽然我没有研究过形式化方法，但我的理解是它们通常用于生命攸关的系统中。如果你不是在构建失败可能导致整个公司死亡或倒闭的东西，那么使用形式化方法可能是矫枉过正的。
通信也是一个大问题。即使您正在构建的东西不是“生命攸关的”，将您围绕系统部分的沟通形式化仍然会有所帮助。
@ThomasOwens 英特尔在臭名昭著的 FDIV 错误之后开始使用形式验证。这不是第一个 CPU 错误，但它很容易重复并在 1994 年的 moniez 中量化为 4 亿美元

【解决方案2】：

这里要问的真正问题不是是否使用它们，而是得到什么和失去什么。

生产力和成果会超过所需的复杂性和学习吗？

【讨论】：

【解决方案3】：

一般来说，您应该使用团队认为合适的方式。对于新项目，会有一个学习曲线，这意味着会有关于过程和所犯错误的问题。您的部分开发时间表将用于纠正这些问题，如果您将来不打算在这个团队中使用它们，那么您实际上不会通过引入新事物来获得长期收益。改变过程需要很长时间和大量的工作。

如果你估计有足够的时间来处理这些问题，你可能会没事.....如果你的估计是正确的。考虑到你没有和这些人一起工作过（至少你的帖子听起来是这样的），你的时间表可能不会像它应该的那样准确，这意味着你可能没有分配足够的时间来完成项目更不用说引入新工艺了。

您必须问自己的另一个问题是“您对要实施的流程感觉如何？”我从不尝试在项目中引入新流程，除非我知道如果必须的话我可以带领团队完成它。不时尝试新事物固然不错，但您需要有一个熟悉的团队，知道如何摆脱困境。

【讨论】：

【解决方案4】：

我一直在研究“轻量级”形式方法的几种方法，用于可能是关键任务但不是生命/安全关键的应用程序。一些想法：

【讨论】：

这是一个很好的列表。最近，我一直在研究 JML 和 Spec# 等代码级的东西。这更符合 Kevin 之前所说的，“总的来说，你应该使用团队觉得舒服的东西。”团队已经对代码感到满意，所以我越接近代码，他们的工作就会越好。

【解决方案5】：

有一些使用 ACSL（ANSI C 规范语言）的成功例子，它拥有一套成熟的工具，其中大部分是开源的，例如 Why 平台、Frama-C。对于Java 类似的技术称为JML（Java 建模语言）。我认为两者都用于嵌入式应用程序的中小型项目，它们有助于在您的代码中添加一些保证，但并非旨在验证规范。 Z 绝对不是用户友好的，并且缺乏足够的工具支持恕我直言。

在可用于规范阶段的商业工具中，我会研究基于 B 方法的罗丹平台。

【讨论】：

【解决方案6】：

在游戏后期，但您可能会考虑使用 testable architecture through Savara 之类的东西，我们在许多以组件之间的通信或交互为主的项目中使用它。这在任何 SOA 后端到 Web 前端中最常见。

它正式基于 pi-calculus，您无需了解 pi-calculus 即可使用它。

【讨论】：

【解决方案7】：

我完全同意汤姆的观点并提出同样的问题，

生产力和成果会超过所需的复杂性和学习吗？

在我看来，除非系统/软件可以被识别为“安全关键”的形式方法是不必要的。

安全关键是什么意思：

当计算机系统的故障可能导致灾难性后果，例如生命损失、环境破坏或系统本身损坏时，这种系统被称为“安全关键型”。

【讨论】：

【解决方案8】：

我同意 Tom 和 Abufardeh 的观点 - 生产力和成果会超过所需的复杂性和学习吗？

此外，这种方法是否更适合在开发之前获取所有需求（并确保这些需求既定义明确又可测试）？首先获取所有需求似乎是常识，但大部分程序并行执行操作，认为稍后获取一些需求是没有问题的。需求蔓延是一场噩梦！电影“五角大楼战争”让任何不同意的人大开眼界。

【讨论】：