我是一名软件工程师/架构师，专注于人工智能和分布式系统，我来自电子和通信工程背景。
在我的软件之旅中，我一直想知道为什么这个工程分支缺乏正式的设计方法，如电子学（数学建模和实现）以及具有许多约束的最佳通信系统的设计，这些系统中的大多数都是比地球上最复杂的软件（比如运行我们使用和开发的软件的 IC）复杂得多，并且唯一具有正式方法的软件相关领域是硬件描述语言。
我最近了解到，存在用于软件设计、规范和验证的形式化方法，如 Z 符号和语言、维也纳开发方法和 b 语言。
但是这个领域的最新技术是什么，普通工程师如何使用它（例如在我的团队中）？
我完全同意你的观点，当今软件开发中使用的正式方法很少。您提到的方法似乎对软件行业的工作没有太大影响（据我所知）。
到目前为止，我已经看到了一些确保满足软件产品需求的方法：
对于这些活动中的每一项，都有许多可用于支持开发的工具。
典型问题：
这实际上与其他工程学科中使用的方法完全不同，但希望能让您对可以仔细研究的内容有所了解。
形式规范和验证方法 (FM) 的“最新技术”足以极大地提高正在开发的系统的质量，但是最大的障碍不是技术（在大多数情况下），而是业务决策——这通常归结为时间和金钱。
一般的软件开发人员没有接受过有效使用 FM 的培训，并且项目计划（通常）不是这样，您可以在不影响截止日期的情况下注入大量建模活动。
这种增加的时间/金钱在更高风险的工作中是可以接受的，例如“关键任务系统”，其中失败的成本是伤害、死亡或巨大的经济损失，但对于开发失败成本在“范围nuisance”（重新启动应用程序、恢复备份等）
在我看来，FM 从业者面临的真正突出挑战在于方法的可用性，以及将它们集成到更敏捷（或不那么“预先设计大”）的开发过程中。
最后，作为一门学科，我们非常习惯于经验测试/验证——在当代开发商店（除了上述“关键任务”团队之外），严格证明系统正确的概念并不经常被考虑或讨论。