Bridging the Gap Between Informal Requirements and Formal Specifications Using Model Federation
Bridging the Gap Between Informal Requirements and Formal Specifications Using Model Federation
复制标题
使用模型联合弥合非正式需求和正式规范之间的差距
DOI：
--
复制
发表时间：
2018
期刊：
影响因子：
--
通讯作者：
Sylvain Guérin
中科院分区：
文献类型：
--
作者：
F. R. Golra;F. Dagnat;J. Souquières;Imen Sayar;Sylvain Guérin
寻求高精度的软件开发项目早在需求工程阶段就采用了正式的方法。然而，未来系统的客户视角是在非正式的需求文件中提出的。正式和非正式方法（以及它们使用和生成的工件）之间的差距进一步增加了本已严格的软件开发任务的复杂性。我们的目标是使用半正式建模技术（模型联合），通过客户端非正式需求文档与开发人员正式规范之间的细粒度可追溯性来弥合这一差距。需求工程过程可以利用这种级别的可追溯性来执行涉及这些非正式和正式工件之一或两者的不同操作。开发这种级别的可追溯性所消耗的精力和时间会在开发项目的后期阶段得到回报。例如，在分析阶段可以准确地缩小导致证明义务不一致的要求范围。我们使用起落架系统案例研究中的运行示例来说明我们的方法。
Software development projects seeking a high level of accuracy reach out to formal methods as early as the requirements engineering phase. However the client perspective of the future system is presented in an informal requirements document. The gap between the formal and informal approaches (and the artifacts used and produced by them) adds further complexity to an already rigorous task of software development. Our goal is to bridge this gap through a fine-grained level of traceability between the client-side informal requirements document to the developer-side formal specifications using a semi-formal modeling technique, model federation. Such a level of traceability can be exploited by the requirements engineering process for performing different actions that involve either or both these informal and formal artifacts. The effort and time consumed in developing such a level of traceability pays back in the later phases of a development project. For example, one can accurately narrow down the requirements responsible for an inconsistency in proof obligations during the analysis phase. We illustrate our approach using a running example from a landing gear system case study.