SMT-Based Model Checking of Industrial Simulink Models
SMT-Based Model Checking of Industrial Simulink Models
复制标题
基于 SMT 的工业 Simulink 模型模型检查
DOI：
10.1007/978-3-031-17244-1_10
复制
发表时间：
2022
期刊：
影响因子：
--
通讯作者：
Hideaki Takai
中科院分区：
文献类型：
--
作者：
Daisuke Ishii;Takashi Tomita;Toshiaki Aoki;The Quyen Ngo;Thi Bich Ngoc Do;Hideaki Takai
嵌入式系统的开发需要对模型进行形式化分析，例如使用 MATLAB/Simulink 描述的模型。然而，工业模型日益复杂使得分析变得困难。本文提出了一种使用 SMT 求解器对 Simulink 模型进行模型检查的方法。所提出的方法旨在 (1) 对复杂模型进行自动、高效和可理解的验证，(2) 对模型进行数值精确分析，以及 (3) 使用 SMT 求解器（我们使用 Z3）演示 Simulink 模型的分析。它首先将目标模型编码为数学算术和位向量领域的谓词逻辑公式。我们探索如何精确编码各种 Simulink 模块。然后，该方法使用基于 k 归纳的算法验证给定的不变性属性，该算法提取涉及目标块的子系统并增量展开执行路径。在实验中，我们将所提出的方法和其他工具应用于一组模型和属性。我们的方法成功验证了大多数属性，包括那些未使用其他工具验证的属性。
The development of embedded systems requires formal analysis of models such as those described with MATLAB/Simulink. However, the increasing complexity of industrial models makes analysis difficult. This paper proposes a model checking method for Simulink models using SMT solvers. The proposed method aims at (1) automated, efficient and comprehensible verification of complex models, (2) numerically accurate analysis of models, and (3) demonstrating the analysis of Simulink models using an SMT solver (we use Z3). It first encodes a target model into a predicate logic formula in the domain of mathematical arithmetic and bit vectors. We explore how to encode various Simulink blocks exactly. Then, the method verifies a given invariance property using thek-induction-based algorithm that extracts a subsystem involving the target block and unrolls the execution paths incrementally. In the experiment, we applied the proposed method and other tools to a set of models and properties. Our method successfully verified most of the properties including those unverified with other tools.