Translating SysML Activity Diagrams for nuXmv Verification of an Autonomous Pancreas
Translating SysML Activity Diagrams for nuXmv Verification of an Autonomous Pancreas
复制标题
DOI：
10.1109/compsac54236.2022.00260
复制
发表时间：
2022-06
期刊：
影响因子：
--
通讯作者：
Orion Staskal;Josh Simac;Logan Swayne;Kristin Yvonne Rozier
中科院分区：
文献类型：
--
作者：
Orion Staskal;Josh Simac;Logan Swayne;Kristin Yvonne Rozier
基于模型的系统工程（MBSE）提供了一个单一的平台，能够定义复杂的，多学科的系统，但常用的工具，如系统建模语言（SysML）缺乏正式验证和验证这些系统的能力。符号模型检查在与SysML相似的抽象级别的系统模型上操作，提供按钮技术来确保可能的行为集始终遵守时间要求，例如，为了安全操作。我们提出了一种从SysML活动图到流行的符号模型检查器nuXmv的翻译方法，使其在四个主要步骤中进行形式化验证：主模块定义，子模块定义，活动图组织和活动图翻译。我们将这一过程应用于自主式人工胰腺系统（AAPS）作为贸易研究。然后，我们验证和确认AAPS nuXmv模型对一组规格来自AAPS的安全要求。
Model Based Systems Engineering (MBSE) provides a single platform capable of defining complex, multidisciplinary systems, but commonly-used tools such as Systems Modeling Language (SysML) lack the ability to formally validate and verify these systems. Symbolic model checking operates on system models of similar levels of abstraction to SysML, providing a push-button technique for ensuring the possible behavior set always obeys temporal requirements, e.g., for safe operation. We propose a translation method from SysML activity diagrams to the popular symbolic model checker nuXmv to enable their formal verification in four main steps: main module definition, submodule definition, activity diagram organization, and activity diagram translation. We apply this process to the Autonomous Artificial Pancreas System (AAPS) as a trade study. We then verify and validate the AAPS nuXmv model against a set of specifications derived from the AAPS safety requirements.