关闭。这个问题是opinion-based .它目前不接受答案。
想改善这个问题吗？更新问题，以便可以通过 editing this post 用事实和引文回答问题.
4 个月前关闭。
Improve this question
我们的客户希望我们构建一个基于 Web 的富 Internet 应用程序来收集软件需求。基本上，它是一个基于 Web 的案例工具，它遵循从利益相关者那里获取需求的特定过程。我是项目经理，我们仍处于项目的早期阶段。
我一直在考虑使用正式的方法来帮助我的客户和开发人员阐明对工具的要求。我所说的形式方法是指某种形式的建模，可能是基于数学的。我读过并正在考虑的一些内容包括 Z( http://en.wikipedia.org/wiki/Z_notation )、状态机、UML 2.0(可能带有诸如 OCL 之类的扩展)、Petri nets ，以及一些编码级别的东西，如契约(Contract)和前后条件。还有什么我应该考虑的吗？
开发人员经验丰富，但根据所使用的形式主义，他们可能需要学习一些数学知识。
我试图确定我是否值得在这个项目上使用正式的方法，如果是，在多大程度上。我知道“这取决于”，所以对我来说最有用的答案是是/否和支持论点。
如果你参与这个项目，你会使用形式化方法吗？
最佳答案
I've been thinking about using formal methods to help clarify the requirements for the tool for both my client and the developers.
很少有开发人员有形式化方法的经验。我唯一一次看到接受正式方法培训的客户是我们移植时 ZUG 的成员 CADiZ到 Windows。
By formal methods I mean some form of modeling, possibly something mathematically-based. Some of the things I've read about and are considering include Z (http://en.wikipedia.org/wiki/Z_notation), state machines, UML 2.0 (possibly with extensions such as OCL), Petri nets, and some coding-level stuff like contracts and pre and post conditions. Is there anything else I should consider?
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/