论文标题
使用PROM从事件日志中产生植物模型，用于正式验证CPS
Plant model generation from event log using ProM for formal verification of CPS
论文作者
论文摘要
本文使用过程挖掘技术从记录的事件痕迹中介绍了植物模型生成的概念。通过使用OPC UA通信协议在视觉上模拟简单的分布式制造系统来获得事件日志。过程发现α算法用于以Petri Net格式提取过程模型。然后使用以培养皿网络为代表的系统行为，以使用拟议的符号符合IEC 61499标准，以构建基本功能块的ECC。最后，闭环系统的形式验证是在由FB2SMV转换器，符号模型Checker NUSMV和其他代表反调查的工具组成的工具链的帮助下完成的。
This paper introduces the concept of plant model generation from the recorded traces of events using the process mining technique. The event logs are obtained by visually simulating a simple distributed manufacturing system using the OPC UA communication protocol. The process discovery alpha algorithm is used to extract the process model in Petri net format. The system behavior represented in terms of Petri net is then fed to construct the ECC of the basic function block in compliance with IEC 61499 standard using the proposed notation. Finally, the formal verification of the closed-loop system is done with the help of a tool chain that consists of fb2smv converter, symbolic model checker NuSMV, and other tools for representing counter-examples.
