Modelling timed reactive systems from natural-language requirements
Modelling timed reactive systems from natural-language requirements
复制标题
根据自然语言需求对定时反应系统进行建模
DOI：
10.1007/s00165-016-0387-x
复制
发表时间：
2016
影响因子：
1
通讯作者：
Carvalho G
中科院分区：
文献类型：
--
作者：
Carvalho G
在系统开发的最初阶段，通常只记录自然语言需求。然而，作为一种非正式的信息来源，自然语言规范可能是模糊和不完整的;这很难通过人工检查来检测。在这项工作中，我们提出了一个正式的模型，命名为数据流反应系统（DFRS），它可以自动从自然语言的要求，描述功能，反应和时间属性。DFRS还可以用于评估需求是否一致和完整。我们定义了DFRS的两个变化：一个符号和一个扩展的版本。符号DFRS（s-DFRS）是一种简洁的表示，本质上避免了显式表示（可能是无限的）状态集，从而避免了状态空间爆炸问题。我们使用S-DFRS作为从自然语言需求生成测试用例的技术的一部分。在我们的方法中，扩展的DFRS（e-DFRS）是从一个符号动态构建的，可能限于某个界限;以这种方式，有界分析（例如，可达性、确定性、完整性）。我们采用的S-DFRS作为中间表示模型，例如，SCR和CSP，获得测试生成的目的。e-DFRS还可以被视为从其生成的s-DFRS的语义。为了连接这样的语义表示建立在文献中，我们表明，电子DFRS可以被编码为TIOTS：一个替代的定时模型的基础上广泛使用的IOLTS和ioco。为了验证我们的整体方法，我们考虑两个玩具的例子和航空航天和汽车行业的两个例子。测试用例是独立创建的，我们验证了它们都是兼容的相应的e-DFRS模型从符号的。这种验证是在NAT 2 TEST工具的帮助下机械地执行的，该工具支持对此类模型的操作。
At the very beginning of system development, typically only natural-language requirements are documented. As an informal source of information, however, natural-language specifications may be ambiguous and incomplete; this can be hard to detect by means of manual inspection. In this work, we present a formal model, named data-flow reactive system (DFRS), which can be automatically obtained from natural-language requirements that describe functional, reactive and temporal properties. A DFRS can also be used to assess whether the requirements are consistent and complete. We define two variations of DFRS: a symbolic and an expanded version. A symbolic DFRS (s-DFRS) is a concise representation that inherently avoids an explicit representation of (possibly infinite) sets of states and, thus, the state space-explosion problem. We use s-DFRS as part of a technique for test-case generation from natural-language requirements. In our approach, an expanded DFRS (e-DFRS) is built dynamically from a symbolic one, possibly limited to some bound; in this way, bounded analysis (e.g., reachability, determinism, completeness) can be performed. We adopt the s-DFRS as an intermediary representation from which models, for instance, SCR and CSP, are obtained for the purpose of test generation. An e-DFRS can also be viewed as the semantics of the s-DFRS from which it is generated. In order to connect such a semantic representation to established ones in the literature, we show that an e-DFRS can be encoded as a TIOTS: an alternative timed model based on the widely used IOLTS and ioco. To validate our overall approach, we consider two toy examples and two examples from the aerospace and automotive industry. Test cases are independently created and we verify that they are all compatible with the corresponding e-DFRS models generated from symbolic ones. This verification is performed mechanically with the aid of the NAT2TEST tool, which supports the manipulation of such models.
登录
查看更多内容
DOI：
--
发表时间：
2014
期刊：
International Workshop on Artificial Intelligence for Requirements Engineering
影响因子：
--
作者：
Alessio Ferrari;Giuseppe Lipari;S. Gnesi;G. Spagnolo
通讯作者：
G. Spagnolo
从受控自然语言规范生成定时系统的测试用例
DOI：
--
发表时间：
2009
期刊：
2009 Third IEEE International Conference on Secure Software Integration and Reliability Improvement
影响因子：
--
作者：
Matthias Schnelte
通讯作者：
Matthias Schnelte
CSP定时输入输出关系和机械化一致性验证策略
DOI：
--
发表时间：
2013
期刊：
IEEE International Conference on Formal Engineering Methods
影响因子：
--
作者：
Gustavo Carvalho;A. Sampaio;A. Mota
通讯作者：
A. Mota
影响因子：
3.4
作者：
V. Ambriola;V. Gervasi
通讯作者：
V. Gervasi
使用工具评估大量自然语言要求的经验
DOI：
--
发表时间：
2010
期刊：
ACM Symposium on Applied Computing
影响因子：
--
作者：
A. Bucchiarone;S. Gnesi;A. Fantechi;G. Trentanni
通讯作者：
G. Trentanni