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

高可靠性是电气控制设备性能的关键。 PLC结合了计算机技术、自动控制技术和通讯技术，广泛应用于工业过程的自动化。 传统的验证方法无法满足复杂PLC系统的一些要求。 在这个本文提出了一种高效的PLC系统建模和验证方法。 为了保证PLC的高速性能，我们提出了“时间间隔模型”和“通知等待”技术。 它可以减少状态空间并使验证一些复杂的 PLC 系统成为可能。 此外，还获得了从建立的PLC模型到Promela语言的转换，并设计了一个用于PLC系统建模和检查的工具PLC-Checker。 使用PLC-Checker 检查一个经典的 PLC 例子，找到一个反例。 虽然这种逻辑错误发生的概率很小，但可能会导致系统死机。

一、简介

PLC是一种自动控制设备，可以接收来自传感器、计算设备或其他PLC的信息逻辑输入信号，输出处理后的逻辑信号。

控制算法可以使用标准语言编写，例如梯形图 (LD)、结构化文本(ST) 或指令列表 (IL) [1]。

PLC使用可编程语言的技术控制大规模集成电路已广泛应用工业[2]。由于安全关键软件可以对生命或财产造成严重损害，核实安全关键软件已成为不可或缺的一步保证软件质量的必要条件。目前的验证PLC的方法仍然停留在仿真和测试上。但是，它们并不能涵盖所有可能的情况，尤其是 PLC 的设计模型是否满足需求。因此，引入了模型检查技术进入PLC领域。对PLC进行理论分析设计变得很重要。

PLC模型检查的首要步骤是建立PLC模型，比如建立一个模型来自功能图 [3]。 PLC模型侧重于建立时间属性[4]。可以建模通过时间自动机[5]的方法或时间段建模方法[6]。因此模型的状态空间将是与定时自动机相比减少了。无论哪种方式选择，最终可以给出一个抽象模型[7]。如何建立一个好的PLC抽象模型是检验的重中之重。作为手动建模容易引入很多错误，所以建立一个集成的建模和测试工具非常重要，这是本文关注的问题之一。

PLC控制程序在实时操作系统中运行（多任务或单任务）；本文主要基于多任务调度PLC系统。第 2 节文章介绍了建模方法PLC系统。第 3 节给出了该模型的分析和改进，因为我们需要降低伪错误。第四节设计了一个模型检查工具PLC-Checker 检查已建立的模型，包括介绍PLC程序转换成SPIN的方法输入语言 Promela 代码。最后，一个经典的 PLC示例用于检查和关键的计算机示例由 PLC-Checker 发现。

2.PLC建模*

这项工作由 NSFC 60973049、60635020 和 TNList 资助跨学科基础。模型检查分为三个步骤：建模、属性描述和验证。最重要的是如何建立系统模型。在系统中，PLC控制器不是孤立的，而是具有与工作环境、驾驶员和人的交互[8]。因此，这些因素也应该建模。环境、人、PLC控制器在逻辑上相互独立和并行。此外，该模型检查器 SPIN 的输入语言 Promela 专注于关于描述并发，所以从这个想法开始，我们将这些因素构建到几个并发进程中符合 SPIN 的检查，它也将准确地描述系统。为了方便描述，它们将是称为并发实体。 PLC控制器与并发实体通过图像表中的符号。

PLC系统的符号包括I（输入端口）、Q（输出端口）和M（中间继电器）。图1是一个PLC系统模型图。时间间隔建模策略：使用标志哪个特定并发实体的位状态代表状态中的并发实体，没有关于系统时钟。这可能会忽略时间状态的差异，从而简化了 PLC 模型。

建模策略不加系统时钟属性，与原PLC不完全对应模型。那主要是因为加入系统时钟会导致PLC系统模型过大，没有对于模型检查工具来处理这么大模型。对状态建模的起点这是不考虑 PLC 扫描的次数，当经历过迁移。不管扫描多少次经验丰富的，他们都将包括在这个模型中。在换句话说，真实模型将是构建的子集模型（时间间隔模型）。真实的 PLC 环境是复杂的，包括一个

各种硬件和人类行为。以下

我们将对不同种类的PLC环境并发实体进行分析。

1) 硬件实体

PLC系统的硬件实体主要是一些PLC控制的设备。这些设备的状态可以作为PLC控制器的输入。因此，硬件实体与其关联的 I 和 Q 绑定，而硬件有自己的工作流程，这个工作流程是由硬件要求决定的。这个工作流程可以抽象成自动机。该自动机用于描述硬件的工作状态。定义 2.1。硬件实体是一个元组 Env =，其中 Ienv 是与硬件绑定的 I 端口entity，Qenv是与实体绑定的Q端口。 A 是描述实体工作流程的自动机，A 是元组 A =，其中 s0 是 A 的初始状态，S 是状态集合，而 T 是转移集合。硬件实体的状态是 I 符号的子集，并且每个状态的 Is 符号都映射到 {True, False}，I符号不出现的状态可以是True或 False（即：任意行事）。硬件实体的转移直接用 Q 的子集表示符号，表示子集中的所有 Q 符号在同时将推动国家之间的迁移。这硬件实体的状态转移图也需要指定初始状态，转换图从这种状态。

硬件实体的状态转移图是基于符号 I 的划分，时间属性为不考虑。硬件实体状态转换图实际上是硬件实体的抽象被忽略时间，抽象的模拟需要参考的硬件。

2）简单的输出实体仅与 Q 端口绑定的简单输出实体不使用 I 端口，这意味着简单的输出实体没有状态转换图。简单的输出entity是显示PLC工作状态的设备，就像号灯一样。简单输出实体的用法是与 Q 端口绑定，以便 PLC 可以使其逻辑设计。

3) 人类行为实体定义 2.2。人类行为实体是一个元组 Env= < Ienv, A>，其中 Ienv 是 I 端口与硬件实体，Qenv是与实体绑定的Q端口。 A 是描述工作流程的自动机实体，A 是一个元组 A =，其中 s0 是初始A 的状态，S 是状态的集合，T 是状态的集合转移。

人类行为实体与硬件实体类似；它们具有相同的状态定义。很难模拟人的行为，尤其是设计一个PLC涉及到一些个人。作为回应这些困难，人类行为建模应该采取一个迭代过程：首先，一个简单的行为模型是建立使用模型验证；那么，如果没有找到柜台例如，构建并验证更复杂的模型，

直到找到反例或难以更复杂；最后，如果之前没有找到有意义的反例，则生成一个完全随机的人的行为模型（即：人的行为是一个完整的图

所有转移都是真实的）以进行验证。但是，完全随机行为的验证会导致状态空间急剧增加，那么如何选择合适的人类行为模型是建模的难点。如果人的输入比较简单，我们可以使用完全随机的行为建模，否则，你需要认真考虑建立合理模型的人类行为。

我们对PLC环境和人建立模型上面的行为，然后我们将对 PLC 控制器进行建模。 PLC控制器在转动时会处于一个循环中上。

 PLC 从 I 端口读取所有输入。

 PLC 计算所有逻辑单元。

 PLC 设置所有 Q 端口。

PLC进程上的基本单元称为网络。所有网络将按照编号顺序运行设计时设置。

PLC控制器的基本逻辑运算网络包括：S触发器、R触发器、SR触发器、EQ触发器、RS触发器，POS上升沿检测器，NEG下降沿探测器等。对基本逻辑运算网络建模，我们采用直接映射策略，即：PLC控制器模型的网络行为和网络的逻辑行为是完全等价的。哪里触发器, R 触发器, SR 触发器, EQ 触发器, RS 触发器可以直接使用布尔表达式映射到它们的行为。