web-applications - 我应该在我的软件项目中使用形式化方法吗？

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

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

开发人员经验丰富，但根据所使用的形式主义，他们可能必须学习一些数学。

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

如果您从事此项目，您会使用正式方法吗？

最佳答案

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



Z 是一种以集合论为基础的形式方法，它与 UML 之间存在很大差距，UML 是一种带有一些半形式符号(状态机)标记的非正式符号。

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

创建域的 Z 模型可能有值(value)，创建客户端和服务器(或 Petri-net，但我发现 pi 更简单且功能更强大)之间的消息传递的 pi 演算模型可能有值(value)。

域的 Z 模型将提供一组独立于实现的类型约束，其表达能力比任何通用实现语言的类型系统都要强大。

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

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

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

我没有使用正式的按契约(Contract)设计的前后条件，尽管我有时会在评论中添加它们，并且经常在断言中添加它们，并且我对可能违反它们的条件进行单元测试。

关于web-applications - 我应该在我的软件项目中使用形式化方法吗？，我们在Stack Overflow上找到一个类似的问题：https://stackoverflow.com/questions/735609/