我们的客户希望我们构建一个基于 Web 的富 Internet 应用程序来收集软件需求。基本上，它是一个基于 Web 的案例工具，遵循特定流程从利益相关者那里获取需求。我是项目经理，我们仍处于项目的早期阶段。
我一直在考虑使用形式化方法来帮助我的客户和开发人员澄清对工具的要求。我所说的形式方法是指某种形式的建模，可能是基于数学的。我已经阅读并正在考虑的一些内容包括 Z ( http://en.wikipedia.org/wiki/Z_notation )、状态机、UML 2.0（可能带有OCL等扩展）、Petri 网和一些编码合同和前置条件和后置条件等级别的东西。还有什么我应该考虑的吗？
开发人员经验丰富，但根据所使用的形式，他们可能需要学习一些数学知识。
我正在尝试确定我是否值得在这个项目上使用形式化方法，如果是，在多大程度上。我知道“这取决于”，所以对我来说最有帮助的答案是是/否和支持论点。
如果你在这个项目中，你会使用正式的方法吗？
我一直在考虑使用形式化方法来帮助我的客户和开发人员澄清对工具的要求。
很少有开发人员有正式方法的经验。当我们将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 模型是司空见惯的。
我没有使用正式的按合同设计的前置和后置条件，尽管我有时会在评论中添加它们，并且经常在断言中添加它们，并且我对可能违反它们的条件进行单元测试。
这里要问的真正问题不是是否使用它们，而是得到什么和失去什么。
生产力和结果会超过所需的复杂性和学习吗？
一般来说，你应该使用团队认为合适的东西。对于新项目，会有一个学习曲线，这意味着会有关于过程和所犯错误的问题。您的部分开发时间表将用于纠正这些问题，如果您将来不打算在这个团队中使用它们，那么您实际上不会通过引入新事物而获得长期收益。改变过程需要很长时间和大量的工作。
如果你估计有足够的时间来处理这些问题，你可能会没事.....如果你的估计是正确的。考虑到你没有和这些人一起工作过（至少你的帖子听起来是这样的），你的时间表可能不会像它应该的那样准确，这意味着你可能没有分配足够的时间来完成项目更不用说引入新工艺了。
您必须问自己的另一个问题是“您对要实施的过程感觉如何？” 我从不尝试在项目中引入新流程，除非我知道如果必须的话我可以带领团队完成它。不时尝试新事物是好事，但你需要有一个让你感到舒服的团队，知道如何摆脱困境。
在游戏的后期，但您可能会考虑通过 Savara进行可测试架构之类的东西，我们将其用于许多以组件之间的通信或交互为主的项目中。这在任何 SOA 后端到 Web 前端中最常见。
它正式基于 pi-calculus，您无需了解 pi-calculus 即可使用它。
有一些使用 ACSL（ANSI C 规范语言）的成功示例，这些工具具有成熟的工具集，其中大部分是开源的，例如 Why 平台、Frama-C。对于Java 类似的技术称为JML（Java 建模语言）。我认为两者都用于嵌入式应用程序的中小型项目，它们有助于在您的代码中添加一些保证，但并非旨在验证规范。Z 绝对不是用户友好的，并且缺乏足够的工具支持恕我直言。
在可用于规范阶段的商业工具中，我会研究基于 B 方法的罗丹平台。
我完全同意汤姆并提出同样的问题，
生产力和结果会超过所需的复杂性和学习吗？
在我看来，除非系统/软件可以被识别为“安全关键”的正式方法是不必要的。
安全关键是什么意思：
当一个计算机系统的故障可能导致灾难性的后果，例如人命损失、环境破坏或系统本身损坏时，这样的系统被称为“安全关键”。
我同意 Tom 和 Abufardeh 的观点——生产力和成果会超过所需的复杂性和学习吗？
此外，这种方法是否更适合在开发之前获得所有需求（并确保这些需求既定义明确又可测试）？首先获取所有需求似乎是常识，但是大部分程序并行执行操作，认为稍后获取一些需求是没有问题的。需求蔓延是一场噩梦！电影“五角大楼战争”让任何不同意的人大开眼界。