售前咨询-李:13308089138
售前咨询-吴:17760489178 English
前沿资讯 真实、准确的物联网、互联网行业新闻

基于形式的PLC建模与校验方法(下)

你的位置: 网站首页 新闻动态 技术应用
基于形式的PLC建模与校验方法(下)
2022-07-21 23:51:25 阅读: 发布人:纵横智控

4. PLC模型检查

PLC被广泛应用在许多应用中,并且有许多设备;这是一个很大的研究领域。任何PLC工作在包括不同设备和人,所以PLC系统是并发的。同时,一个PLC系统如果有一些错误很难发现,主要是因为逻辑设计错误,但不是计算错误。所以我们专注于PLC的检测程序逻辑过程,而这个逻辑完全可以位逻辑描述。因此,为了简化PLC程序模型,专注于模型检查,我们

进行以下设置:

 PLC是一个逻辑控制程序,所有的控制变量只有0和1两个状态;

 PLC 程序在并发环境中运行。在这种情况下,PLC编程更可能有有些错误不容易发现。

针对以上特点,我们采用模型检查工具 SPIN(我们的工具 PLC-Checker 也实现了 NuSMV)检查。我们制定了一系列的转换规则,将上述模型构建成SPIN的输入语言Pro mela,系统属性也需要翻译成Promela,SPIN 将它们放在一起然后执行检测。

RTU

PROMELA 语言是 C 类语言,它们是语义相似。所以我们只举一些例子显示翻译的基本概念。要查看PROMELA 语言的详细信息,请访问 www.spin root.com。我们将介绍 PRO MELA 文件的三个部分作为 SPIN 的输入。

1)PLC控制器代码

PLC控制器由多个网络组成。

PLC控制器的代码也是从网络生成的。当然,在此之前,您应该声明您需要的变量。每个网络都有其输入端口和输出端口,每个端口都可以用布尔表达式表示。我们通过逻辑分配输出端口的值计算所有输入端口。这是翻译PLC网络的方法。

下面是一个转换 SR 网络的例子:

如果

:: Exp(R) == 1 -> Q = 0;

::其他->

如果 ::Exp(S) == 1 -> Q = 1;

::else -> 跳过;菲;

菲;

/* Exp(S) 是 S 端口的布尔表达式

Exp(R) 是 R 端口的布尔表达式

Q是输出端口*/

2)并发实体的代码

我们认为每个并发实体都是一个独特的过程,没有不管是人的行为还是设备。这些过程与 PLC 控制器进程共享变量。这必须是确保系统的并发性。在本文的第二部分,我们讨论了所有并发实体被建模为自动机。这自动机的意思是从一种状态转移到另一种状态。我们使用 I 端口来形成实体的状态。利用goto 语句作为转移(就像在汇编语言中一样)。一个简单的例子如下所示:

状态A:

原子{

如果

:: Q1 -> {IB, goto StateB}

:: Q2 -> {IC, goto StateC}

菲;}

/* StateA 是状态 A 的标签

Q1、Q2为转移条件

IB是将状态值设置为状态B的值

goto StateB 表示跳转到 stateB */

3)propertyProperty代码是PLC系统必须遵守的规则。我们使用 LTL(线性时间逻辑)公式作为输入格式。我们应该写相反的财产,因为SPIN的机制。 SPIN 会发现我们的情况财产发生,那应该是一个反例。我们不能直接写 LTL 公式,而是使用 ing 宏。首先我们应该定义所有的命题

在 LTL 中的宏中(如 #define p i5 == 0),那么我们使用定义的命题来形成 LTL 公式。旋转可以使用“SPIN-f”指令自动将 LTL 公式转换为 PRO MELA 代码(查看更多SPIN 手册中的详细信息)。

4) 通知等待机制

在建模讨论中,我们建议不添加时间等待机制。这种机制也需要体现在代码中。具体实现是签一个每个非 PLC 进程的位变量(所有进程PLC 控制器除外)作为信号。当自动机转移到状态标签,信号变量设置为0,并且下一个赋值要求这个变量为 1 才能继续。由于 PROMELA 语法特征,该过程将继续进行。在PLC过程中没有此类限制,相反,PLC 进程可以设置这些变量为1,从而确保每一步都必须走通过至少一次 PLC 扫描来完成就是这样称为通知等待机制。按照上面的四个步骤;我们得到一个完整的代码我们系统的 SPIN 输入文件。然后我们可以使用 SPIN

检查模型。 SPIN模型的操作步骤检查器,请参阅 SPIN 手册(访问 www.spin root.com)。 SPIN会给出是否找到反例的结果,我们可以用理论来分析上面提到了 spin 给出的跟踪文件。

使用这种检测机制,我们开发了一个工具模型检查 PLC-checker。它有助于建立视觉模型和检查的实施荷兰国际集团,并且可以给对结果进行简单分析。 当然,它找到的反例应该手动检查以使确定它是否是一个真正的反例。 然而,随着在trail文件的帮助下,这不是一个非常困难的任务。 我们还成功地使用了一些检查PLC 检查器(显示在下一节中)。 在经典教科书的例子,找到了一个反例。 虽然反例的发生概率非常低,但确实会发生并且可能会产生严重的后果。 这个工具也证明了正确性和本文理论的有效性。

5. 运行 PLC-Checker

我们将通过以下方式展示 PLC 检查器的有效性检查两门通道模型。 两门通道用于防止封闭的房间与外部世界。通过输入梯形图和并发实体进入工具,也就是属性的定义,我们执行一下检查。 图 3 显示了结果。如我们所见,结果中有一个错误。 这是通过检查线索证明是一个真正的反例手动归档。 也就是说我们的机制是有效的在检查此类 PLC 程序时。


6。结论

我们研究PLC的建模和检查理论本文采用形式化方法。 要求分析了PLC建模的特点,通过时间间隔策略建立了并发实体模型。然后我们证明时间间隔模型是一个超集PLC系统,并通过增加无时间等待机制减少模型。 它还确保了所有的变化系统可由PLC控制器扫描。 我们发现通过检查系统的反例来找出系统的错误。 最后,SPIN的使用方式检查模型给出。 还有对应的介绍了模型检查工具PLC-Checker。 在这个阶段,该机制还有很多不完善的地方,比如作为定时器的处理。 但它有伟大而独特的解决状态探索问题的优势。我们仍在积极探索此类问题。


友情链接