Automatic Verification of Behavior of UML Requirements Specifications using Model Checking
Automatic Verification of Behavior of UML Requirements Specifications using Model Checking
复制标题
DOI：
10.5220/0009339001580166
复制
发表时间：
2020
期刊：
影响因子：
--
通讯作者：
Saeko Matsuura;Sae Ikeda;Kasumi Yokotae
中科院分区：
文献类型：
--
作者：
Saeko Matsuura;Sae Ikeda;Kasumi Yokotae
：随着信息和通信技术（ICT）的发展，服务往往是通过相互操作的各种架构的系统集合来提供的。除了传统的功能需求之外，系统开发还必须包含非功能需求。然而，为了确定多个协作系统的要求，有必要a）考虑硬件架构、用户特性和系统安全要求，b）在开发的早期阶段验证这些。 UML 是一种众所周知的通用建模语言，通过它可以定义功能需求并支持基于指定用例模型的设计和实现工作。然而，使用 UML 中的用例模型很难验证这种系统间协作。此外，使用 UML 中的静态模型来确认多个互操作系统的系统同时表现出的正确行为是很困难的。本研究提出了一种方法，将 UML 描述的相互协作的多个系统的模型转换为使用模型检查工具 UPPAAL 的模型，并验证是否可以在没有死锁的情况下发生并行行为。从而论证了一种在开发早期应用的、保证多系统并发操作和协作正确性的方法。
: With the development of information and communication technology (ICT), services have often been provided through a collection of systems of various architectures interoperating with each other. System development must incorporate non-functional requirements in addition to traditional functional requirements. However, to determine the requirements of multiple cooperative systems, it is necessary a) to consider hardware architecture, user characteristics, and system safety requirements and b) to verify these at an early stage of development. UML is a well-known general purpose modeling language through which it is possible to define functional requirements and to support design and implementation efforts that are based on a specified use case model. However, it is difficult to verify such inter-system cooperation using use case models in UML. Moreover, confirming the correct behaviors, exhibited concurrently, of a system of multiple interoperating systems is difficult using the static models found in UML. This study proposes a method of transforming a model of mutually cooperating multiple systems described in UML into a model that uses the model-checking tool UPPAAL and verifying whether parallel behaviors can occur without deadlock. Consequently, a method, applied at an early stage of development, of guaranteeing the correctness of the concurrent operation and cooperation of multiple systems is demonstrated.