| 摘 要: 在工业4.0背景下,离散事件仿真模型的规模与复杂性与日俱增。本文主要研究如何从根本上保证该系统行为的可靠性,从而在一定程度上避免由于系统逻辑错误所带来的巨大损失。为此,本文提出一种基于NuSMV的离散事件仿真模型的形式化分析与验证方法。该方法首先提取系统行为并将其转换为SMV代码。然后,该方法提出系统性能需求并将其实例化可检验的形式化属性。其次,将SMV代码与形式化属性结合,通过NuSMV模型检测器进行验证。最后,本文通过工业生产的案例来说明方法的可行性。 |
| 关键词: 离散事件仿真模型 模型检测 形式化分析与验证 |
|
中图分类号: TP
文献标识码:
|
|
| Formal Analysis and Verification of Discrete-Event Simulation Models |
|
LIU Hui1, QI Yunsong2
|
1.Jiangsu University of Science and Technology;2.mailqys@163.com
|
| Abstract: In the context of Industry 4.0, the scale and complexity of discrete-event simulation models are increasing rapidly. This paper investigates how to fundamentally guarantee the behavioral reliability of such systems, thereby mitigating, to a considerable extent, the substantial losses caused by logical errors within the system. To this end, this paper proposes a formal analysis and verification approach for discrete-event simulation models based on NuSMV. The proposed approach first extracts the system behavior and transforms it into SMV code. It then identifies the system performance requirements and instantiates them as verifiable formal properties. Subsequently, the SMV code and the formal properties are combined and submitted to the NuSMV model checker for verification. Finally, the feasibility of the proposed approach is demonstrated through a case study of an industrial production scenario. |
| Keywords: discrete-event simulation models, model checking, formal analysis and verification |
