基于形式的PLC建模与校验方法（下）

4. PLC模型检查

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

进行以下设置：

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

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

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

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。 在这个阶段，该机制还有很多不完善的地方，比如作为定时器的处理。 但它有伟大而独特的解决状态探索问题的优势。我们仍在积极探索此类问题。