An Approach of Requirements Tracing in Formal Refinement
An Approach of Requirements Tracing in Formal Refinement
复制标题
形式细化中的需求追踪方法
DOI：
--
复制
发表时间：
2010
期刊：
影响因子：
--
通讯作者：
Aryldo G. Russo
中科院分区：
文献类型：
--
作者：
M. Jastram;S. Hallerstede;M. Leuschel;Aryldo G. Russo
计算系统的形式化建模产生的模型旨在针对已形式化的需求是正确的。典型计算系统的复杂性可以通过逐步引入所有必要细节的形式细化来解决。我们报告了我们在跨细化级别将非正式自然语言需求追踪到正式模型中所获得的初步结果。该方法使用 WRSPM 参考模型进行需求建模，使用 Event-B 进行形式建模和形式细化。 WRSPM 的基本细化概念促进了 WRSPM 和 Event-B 的组合使用，它为跟踪需求到正式细化提供了基础。
我们假设需求是不断变化的，这意味着我们必须应对需求模型和形式模型的频繁变化。我们的方法能够利用 Event-B 方法中内置的相应技术来处理频繁的变化。
Formal modeling of computing systems yields models that are intended to be correct with respect to the requirements that have been formalized. The complexity of typical computing systems can be addressed by formal refinement introducing all the necessary details piecemeal. We report on preliminary results that we have obtained for tracing informal natural-language requirements into formal models across refinement levels. The approach uses the WRSPM reference model for requirements modeling, and Event-B for formal modeling and formal refinement. The combined use of WRSPM and Event-B is facilitated by the rudimentary refinement notion of WRSPM, which provides the foundation for tracing requirements to formal refinements.
We assume that requirements are evolving, meaning that we have to cope with frequent changes of the requirements model and the formal model. Our approach is capable of dealing with frequent changes, making use of corresponding techniques already built into the Event-B method.
DOI：
10.1007/978-3-642-14521-6_4
发表时间：
2010
期刊：
--
影响因子：
--
作者：
Cavalcanti A
通讯作者：
Cavalcanti A