我应该在我的软件项目中使用正式的方法吗?

我一直在考虑使用正式的方法来帮助澄清我的客户和开发人员对该工具的需求。

很少有开发人员有正式的方法经验。我唯一一次见到接受过正规方法培训的客户是我们移植时祖格的成员。 CADiZ 到Windows。

我指的是某种形式的建模,可能是基于数学的。我读过的一些东西包括Z( http://en.wikipedia.org/wiki/Z_notation ,状态机,UML2.0(可能带有OCL等扩展),Petri网,以及一些编码级的东西,比如契约和前后条件。还有什么需要考虑的吗?

Z是一种以集合论为基础的形式方法,而UML是一种带有标记的半形式符号(状态机)的非正式符号,两者之间有很大的差距。

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

创建域的z模型可能有价值,在客户机和服务器(或者Petri网)之间创建消息传递的pi演算模型也可能有价值,但我发现pi既简单又强大。

域的z模型将给出一组与实现无关的类型约束,这些约束比任何公共实现语言的类型系统都更有力地表达出来。

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

UML模型给你的是一个符号,它将一个大系统分解成功能区(包图),静态地显示那些区域中的类如何相互关联(类图),动态地显示那些类的实例如何关联(序列图、活动图和交互图),以及如何部署包。(组件和部署图)。这些方法对于团队中的交流很有用,也有助于使想法更加充实,但是没有正式定义的语义,这使得分析非常复杂。

我在90年代与之合作的z专家认为在z中指定一个case gui的想法很荒谬。为这样的GUI创建UML模型是司空见惯的。

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

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

生产力和成果是否会超过所需的复杂性和学习?

一般来说,你应该使用团队喜欢的东西。对于新的项目,会有一个学习曲线,这意味着会有关于过程和所犯错误的问题。开发时间表的一部分将用于纠正这些问题,如果您不打算在将来将这些问题与此团队一起使用,那么实际上,通过引入新的内容,您将不会获得长期收益。改变过程需要很长的时间和大量的工作。

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

你必须问自己的另一个问题是“你对你想要实现的过程有多满意?”我从不尝试在一个项目中引入一个新的过程,除非我知道如果必须的话,我可以让团队通过它。时不时地尝试新事物是件好事,但是你需要有一个你能适应的团队来知道如何走出困境。

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

• Alloy
• SysML
• SPIN
• Others???

使用AcSL(ANSI C规范语言)有一些成功的例子,这些工具具有成熟的工具集,其中大部分是开源的,例如为什么平台,FRAMA.C,Java类似的技术,称为JML(Java建模语言)。我认为两者都用于嵌入式应用程序的中小型项目,它们有助于在代码中添加一些保证,但并不旨在验证规范。Z绝对不是用户友好的,缺乏足够的工具支持imho。

在可用于规范阶段的商业工具中,我将研究基于B方法的Rodin平台。

在比赛后期,你可能会考虑 testable architecture through Savara 我们在许多项目中使用,在这些项目中,组件之间的通信或交互占主导地位。这在Web前端的任何SOA后端中都很常见。

它正式以π微积分为基础,你不需要理解π微积分就可以使用它。

我完全同意汤姆的看法,并问同样的问题,

生产力和成果是否会超过所需的复杂性和学习?

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

安全关键是什么意思:

当计算机系统的故障可能导致灾难性后果,如人身伤亡、环境破坏或系统本身损坏时,这种系统被称为安全关键。

我同意汤姆和阿布法德赫的观点——生产力和成果是否会超过所需的复杂性和学习?

此外,这种方法是否更好地在开发之前获得所有需求(AMD确保这些需求是定义良好的和可测试的)?先得到所有的需求似乎是常识,但是大部分程序并行地做一些事情,认为以后得到一些需求是没有问题的。需求蔓延是一场噩梦!电影《五角大楼战争》让任何不同意的人大开眼界。