Verifying the structure and behavior in UML/OCL models using satisfiability solvers
Verifying the structure and behavior in UML/OCL models using satisfiability solvers
复制标题
DOI：
10.1049/iet-cps.2016.0022
复制
发表时间：
2016-12
期刊：
影响因子：
--
通讯作者：
Nils Przigoda;Mathias Soeken;R. Wille;R. Drechsler
中科院分区：
文献类型：
--
作者：
Nils Przigoda;Mathias Soeken;R. Wille;R. Drechsler
由于嵌入式和网络物理系统的复杂性越来越不断增加，因此依赖建模语言（例如统一建模语言（UML）/对象约束语言（OCL））的相应设计解决方案引起了人们越来越多的关注。由于正式验证技术的最新成功，UML/OCL模型还允许在设计阶段的早期阶段验证和/或检查给定模型的某些属性。为此，已经提出了不同的验证和验证方法。在这项工作中，作者激励，定义和描述结构性的不同验证任务以及行为UML/OCL模型，这些模型可以使用求解器来解决布尔值。他们描述了如何将这些验证任务转化为符号公式，然后将其传递给现成的求解器。获得的结果使设计师能够得出有关所考虑模型的正确性的结论。
Due to the ever increasing complexity of embedded and cyber-physical systems, corresponding design solutions relying on modelling languages such as Unified Modelling Language (UML)/Object Constraint Language (OCL) find increasing attention. Due to the recent success of formal verification techniques, UML/OCL models also allow to verify and/or check certain properties of a given model in early stages of the design phase. To this end, different approaches for verification and validation have been proposed. In this work, the authors motivate, define, and describe different verification tasks for structural, as well as behavioural UML/OCL models that can be solved using solvers for Boolean satisfiability. They describe how these verification tasks can be translated into a symbolic formulation which is passed to off-the-shelf solvers afterwards. The obtained results enable designers to draw conclusions about the correctness of the considered model.