Modularization of Refinement Steps for Agile Formal Methods
Modularization of Refinement Steps for Agile Formal Methods
复制标题
敏捷形式方法的细化步骤的模块化
DOI：
10.1007/978-3-319-68690-5_2
复制
发表时间：
2017
期刊：
影响因子：
--
通讯作者：
G. Saake
中科院分区：
文献类型：
--
作者：
F. Benduhn;T. Thüm;I. Schaefer;G. Saake
敏捷方法和形式化方法的结合已经被认为是一个很有前途的研究领域。然而，许多正式的方法依赖于基于细化的开发过程，这给它们集成到敏捷过程中带来了问题。我们认为细化层次结构中的冗余是逐步细化的实际应用的一个挑战，并提出了基于叠加的细化步骤模块化作为一个潜在的解决方案。虽然传统上，精化层次结构中的每个模型都必须单独开发和维护，但我们的概念允许开发人员指定将模型转换为精化模型的精化步骤。我们已经开发了支持AsmetaL语言的工具，并通过案例研究评估了我们的方法。结果表明，对于地面模型和四种细化，开发工件的复杂性在总体尺寸方面减少了48.6%。此外，案例研究表明，基于叠加的细化简化了勘探开发和应对不断变化的需求的替代细化的开发。因此，我们认为这项工作是朝着敏捷形式化方法迈出的一步，这些方法是为支持迭代开发而量身定制的，促进了它们与敏捷开发过程的结合。
The combination of agile methods and formal methods has been recognized as a promising field of research. However, many formal methods rely on a refinement-based development process which poses problems for their integration into agile processes. We consider redundancies within refinement hierarchies as a challenge for the practical application of stepwise refinement and propose superimposition-based modularization of refinement steps as a potential solution. While traditionally, each model in a refinement hierarchy must be developed and maintained separately, our concept allows developers to specify the refinement steps that transform a model into a refined one. We have developed tool support for the language AsmetaL and evaluated our approach by means of a case study. The results indicate a reduction of complexity for the development artifacts in terms of their overall size by 48.6% for the ground model and four refinements. Furthermore, the case study shows that superimposition-based refinement eases the development of alternative refinements for exploratory development and to cope with changing requirements. Thus, we consider this work as a step towards agile formal methods that are tailored to support iterative development, facilitating their incorporation into agile development processes.
登录
查看更多内容
DOI：
10.1007/978-3-642-27919-5
发表时间：
2012
期刊：
J. Univers. Comput. Sci.
影响因子：
--
作者：
D. Kourie;B. Watson
通讯作者：
B. Watson
面向 Delta 编程的 Liskov 原理
DOI：
10.1007/978-3-642-34026-0_4
发表时间：
2012
期刊：
Software - Practice and Experience
影响因子：
--
作者：
Reiner Hähnle;Ina Schaefer
通讯作者：
Ina Schaefer
安全关键系统的严格开发流程：从 ASM 模型到 Java 代码
DOI：
10.1007/s10009-015-0394-x
发表时间：
2015
影响因子：
1.5
作者：
Paolo Arcaini;A. Gargantini;E. Riccobene
通讯作者：
E. Riccobene
使用三值模型检查对开放特征进行模块化验证
DOI：
--
发表时间：
2005
期刊：
International Conference on Automated Software Engineering
影响因子：
--
作者：
Harry C. Li;S. Krishnamurthi;Kathi Fisler
通讯作者：
Kathi Fisler
软件产品线的模块化定理：Jbook 案例研究
DOI：
--
发表时间：
2008
期刊：
Journal of universal computer science (Online)
影响因子：
--
作者：
D. Batory;E. Börger
通讯作者：
E. Börger