Mic*_*ael 4 modeling formal-verification formal-methods requirements web-applications
我们的客户希望我们构建一个基于Web的富Internet应用程序来收集软件需求.基本上,它是一个基于Web的案例工具,遵循从利益相关者那里获取需求的特定流程.我是项目经理,我们还处于项目的早期阶段.
我一直在考虑使用正式的方法来帮助我的客户和开发人员澄清该工具的要求.通过形式方法,我的意思是某种形式的建模,可能是基于数学的.我读过并正在考虑的一些内容包括Z(http://en.wikipedia.org/wiki/Z_notation),状态机,UML 2.0(可能带有OCL等扩展),Petri网和一些编码合同以及前后条件等级别的东西.还有什么我应该考虑的吗？
开发人员经验丰富,但根据使用的形式主义,他们可能需要学习一些数学.
我试图确定是否值得我在这个项目上使用正式方法,如果是这样,在多大程度上.我知道"这取决于"所以对我来说最有用的答案是肯定/否定和支持论点.
如果你参加这个项目,你会使用正式的方法吗？
Pet*_*ham 10
我一直在考虑使用正式的方法来帮助我的客户和开发人员澄清该工具的要求.
很少有开发人员有正式的方法经验.当我们将CADiZ移植到Windows 时,我唯一一次看到正式方法培训的客户是ZUG的成员.
通过形式方法,我的意思是某种形式的建模,可能是基于数学的.我读过并正在考虑的一些内容包括Z(http://en.wikipedia.org/wiki/Z_notation),状态机,UML 2.0(可能带有OCL等扩展),Petri网和一些编码合同以及前后条件等级别的东西.还有什么我应该考虑的吗？
Z是一种非常大的差距,它是一种形式的方法,以集合论为基础,而UML是一种非正式的符号,带有一些标记的半正式符号(状态机).
一些技术客户,例如您期望使用软件需求工具,对UML非常熟悉.
创建域的Z模型可能有价值,在客户端和服务器(或者petri网之间)创建消息传递的pi-calculus模型可能很有价值,但我发现pi更简单,更强大.
您的域的Z模型将给出一个独立于实现的类型约束集,表示比任何常见实现语言的类型系统更强大.
您的消息传递的正式模型将为您提供运行分析的工具,以确保您不会丢失更新或发生冲突或死锁.
UML模型给你的是一个用于将大型系统分解为功能区域(包图)的表示法,用于显示这些区域中的类如何静态地相互关联(类图),以及如何动态地显示这些类的实例(序列,活动和交互图),并显示如何部署包(组件和部署图).这些对于团队中的沟通很有用,并且可以稍微充实一些想法,但是没有正式定义的语义,这允许非常复杂的分析.
我在90年代与之合作的Z专家考虑过在Z中指定一个CASE GUI的想法.为这样的GUI创建UML模型是司空见惯的.
我没有使用正式的按合同设计的前后条件,虽然我有时会在评论中添加它们,并经常在断言中添加它们,并且我会对可能违反它们的单元测试条件进行单元化.
| 归档时间： |
|
| 查看次数： |
1774 次 |
| 最近记录： |