基于PLCopen运动控制功能块的时间自动机建模与验证

孙青怡，黄志韬

（杭州电子科技大学 计算机学院，杭州 310018）

0 引言

PLCopen组织制定的运动控制功能块[1]是基于IEC61131-3 标准定义的一组功能块语言，主要是在IEC的研发环境中加入运动控制技术，采用统一接口以提高代码复用性和系统可重构性，具有统一的编程规范，功能块直观性强，使用功能块图语言能够使编程调式时间大大减少。随着运动控制系统的不断发展和日益复杂，需要提高系统的安全性和可靠性[2]。运动控制系统的安全性验证问题[3]是验证工业控制系统建模的关键问题，目前缺少针对该系统的验证方法，而传统的验证方法很少考虑到验证难度、验证时间以及验证模型可重用性的问题。在我们的工作中，我们讨论了PLCopen运动控制功能块的可靠性验证。

D.Aza-Vallina[4]等人描述了个现场总线的行为，他们使用mode自动机（mode-automata）而不是传统的马尔可夫链方法对这些行为进行建模,该方法可以缩小模型的状态空间但是没有对时间进行建模，所以无法验证系统的实时性。Y.Jiang[5]将可编程控制器的程序的逻辑模块以及硬件组件抽象成贝叶斯结点，再将它们映射到贝叶斯网络中，从而得出系统运行错误的概率。De Silva和Dias等[6]提出了一种基于模型的方法来验证安全仪表系统（SIS）。在这种方法中，由国际自动化协会（ISA）描述的规范和FBD程序被自动转换为时间自动机模型，然后使用Uppaal测试工具验证安全仪表系统是否符合规范模型。F.Basile[7]提出了一个基于事件驱动的方法来辅助功能块图程序的设计。该方法将每一个功能块实例抽象成一个对象，并且这些对象的执行由具体的事件来驱动。

迄今为止，以功能块实现的运动控制系统，还缺乏相关的形式化验证研究。因此，提出一种PLC执行模型和转换算法来形式化运动控制功能块，通过Uppaal检测系统[8]来验证程序的可靠性。

1 PLC执行模型

功能块图程序在循环中扫描执行程序，将可编程控制器扫描周期过程转换为时间自动机模型，这个模型作为功能块的循环执行模型来描述可编程控制器的执行阶段。自动机模型决定了一个自动机实例的行为，定义一个模型模板主要包括它的局部变量、常量、Location集合以及Edge集合。首先对时间自动机模型中的Location进行结构化定义，可将状态定义为一个四元组如定义1所示。

定义1 TA模型的Location：

1）name描述该状态名称，是在一个模型模板中状态的唯一标识，类型为字符串；

2）rate指定指数分布参数，规定了系统在该状态的停留时间满足的指数分布的参数，类型为字符串；

3）invariant指定状态约束条件，描述了系统位于该状态必须满足的条件，类型为字符串；

4）type指定状态结点的类别，包括initial、urgent和committed三个类别，initial用于指定该状态是否为初始状态，urgent用于指定该状态是否为紧急状态，committed用于指定该状态是否为提交状态，类型都为布尔变量。

根据可编程控制器的执行流程生成执行模型，用于模拟周期之间的执行状态转换，模型如图1所示。其中Idle状态是时间自动机的初始状态l0，Input、Execute、Output、Update、Next、End状态是一个功能块执行时的不同阶段，当自动机进入Input状态并以Next状态结束时为一个周期。

图1 可编程控制器循环执行模型

上述执行模型根据以下几个状态结点来描述PLC扫描周期的执行阶段：

这些状态中，Idle表示当前可编程控制器处于空闲状态，变量IN表示当前功块已扫描的输入引脚序号，OUT表示当前功能块的输出引脚序号，变量N表示当前功能块图程序的功能块实例个数。当可编程控制器开始执行之后，模型状态会从Idle转换到Input状态，表示当前功能块图程序中功能块实例使能并且开始读取输入数据。随着input()函数的执行，模拟读取输入变量，由于功能块读取输入引脚时，会判断功能块是否使能以及参数是否合法等选择不同处理方式，所以通过Input状态和Execute状态之间的循环转换模拟功能块读取输入引脚的过程。输入引脚扫描结束之后将会从Execute状态切换到Output状态，calculate()函数表示功能块会根据输入引脚计算轴状态（错误信息或预处理）、目标位置、目标速度、目标加速度等等信息，所以也设置循环转换模拟不断查询参数与状态信息。Output状态到Update状态的转换模拟判断轴是否达到目标位移，通过Output()函数表示修改轴信息结构体的过程。Update状态切换到Next状态表示一次循环控制结束。对于循环执行模型，变量FBN表示是否还有新的功能块输入，如果有新的输入代表可编程控制器将执行新的循环并且将输入序号IN和输出序号OUT重新置1，否则代表程序执行结束。简单来说，一个功能块实例的执行会更新系统环境中的变量。

2 功能块图程序建模

一个FBD程序的结构化描述如定义2所示：

定义2 FBD程序：

其中：

1）FBDname：功能块图程序的名称，一般会命名来体现本段程序的内容；

2）Nodes：功能块实例的集合，包含一段功能块图程序中的所有功能块实例；

3）FBN：程序网络结构，由功能块实例，以及实例之间的关系组成；

4）IP：一组输入变量，用于表示程序中处理的参数；

5）OP：一组输出变量，即程序执行之后输出的参数；

6）IOP：一组输入输出变量，是轴信息变量，一个结构体参数，具体定义由开发商决定；

7）VL：一组FBD中定义的局部变量参数；

8）VG：一组FBD中定义的全局变量参数；

9）VE：全局外部变量，用于FBD与其他FBD的组织与合并参数；

10）VA：程序中可访问变量；

11）Body：用于描述FBD程序的实例行为；

定义3 连接集合：

其中：

1）Nodes是功能块实例FB的集合。＜FBx，Voutput，FBy，Vinput是其中一个连接，可表示为FBnamei.opm→FBnamej.ipn；

2）FB以及FBy分别代表两端的功能块实例；

3）Voutput∈FBoutput以及Vinput∈FBinput分别代表两个功能块实例的输出端口和输入端口。

定义4 功能块实例：

其中：

1）FBname：是该功能块实例的名字；

2）FBTypeName：是该实例相应的功能块类型名称。

3）executeOrder：是该功能块相对其他功能块的执行顺序。它是一个定义功能块实例的执行顺序的整数。每个功能块中心的数字则代表功能块实例执行的顺序executeOrder，需要注意executeOrder是在执行顺序有歧义的情况下才有效果。

在把功能块图程序转换为时间自动机模型之前，功能块实例的执行顺序也必须确定。在PLCopen运动控制规范中启动单个轴的运行方式其基本规则是按顺序给出运动控制命令，即使PLC具有实时并行处理能力，也是按顺序执行运动控制命令。功能块图程序的执行顺序是由具体的厂商制定的。

在图2所示功能块图程序中，计数器N代表功能块实例编号，并确保功能块实例一次执行。在扫描最后一个功能块实例之后，计数器将重置以便重复扫描周期。在图2所示的程序片段中，当Start变量设置为true时，mc_fb_1、mc_fb_2的执行顺序存在歧义，可以根据手动设定的executeOrder来判断哪一个功能块先执行。由于图中因此mc_fb_1先执行。由于运动命令依次执行，提取FBD程序的执行列表，然后将其转换为Uppaal模板。

图2 功能块图程序

本小节提出一个Diagram-Uppaal（D-U）转换来执行上述转换。D-U转换的第一步，定义一个Diagram-List（D-L）转换来提取出功能块图的执行列表。由于功能块图的连接有输入端和输出端，可将功能块实例以及逻辑操作（AND/OR）映射为节点，因此连接的输入端为前驱节点，输出端为后继节点，将各节点之间的连接线映射成边，所得到的功能块图程序的图模型称为FBD图，定义一个元组Gi=＜Ni，Fconi＞来描述图模型，其中

例如将图2中的程序用图模型Gi来描述，该图一共有三个功能块实例，映射为三个图，如图3所示。

图3 程序图模型Gi

将该程序中的三个图定义为G1，G2，G3，因此该功能块图之间的连接可描述为：

其中，函数last（G1）返回的是图G1中所有功能块实例的执行结果（此处只有功能块实例mc_fb_1），表示该连接关系中的前驱节点；函数head（G3）返回的是图G3中所有功能块实例的首节点，表示该连接关系中的后继节点。

通过由功能块之间的连接执行D-L转换得到的结构形式为：

其中，fop取决于Nt，Nt代表逻辑表达式，如果Nt是逻辑与（AND），那么fop（Scnd1，Scnd2）执行交运算，如果Nt是逻辑或（OR），那么fop（Scnd1，Scnd2）执行并运算，我们在功能块图上重复执行D-L转换，直到功能块实例上没有逻辑运算。通过转换结果，我们可以生成功能块图程序的执行列表：

D-U转换的第二步，将功能块实例描述为时间自动机中的位置集合，将程序中的功能块连接描述为时间自动机中的边集合。由图2中的功能块程序生成的位置集合如下所示，位置范围从lstart～lEnd。

其中，lfbi表示功能块实例，lstart代表时间自动机的初始位置，lEnd代表时间自动机的最终位置，lEnd是程序单次运行周期的最终状态，在程序下一个周期的运行开始之前，多个自动机将会在同步事件end的作用下切换到初始状态lstart。并且提出以下规则，以便将程序的功能块连接转换为边集合。

时间自动机中的边可以表示为：

规则1：对于start到程序的第一个功能块实例，转换成时间自动机的边

规则2：对于程序的最后一个功能块实例到end，转换成时间自动机的边

规则3：对于其他功能块实例之间的连接关系，转换成时间自动机的边

其中assignmenti()将输入变量传递到输入缓冲区，cndi()获取边的执行条件。

D-U转换完成之后，可以得到基于功能块图程序的时间自动机位置集合以及边集合，将程序转换为时间自动机模型，该模型描述为FBDProgramModel()。

3 实验

以抛球机为例，对实现该系统的程序进行建模。图4(a)中是抛球机器照片以及图4(b)是该机器的示意图。根据示意图，A沿y轴移动，B沿x轴移动。A和B移动到准备位置，通过设置B在y轴的距离和速度实现抛球功能。我们把这部分转换成时间自动机模型来检查功能和性能要求是否得到满足。

图4 抛球机

图2中的功能块图程序是用于实现抛球机功能的部分程序，对该程序进行验证，将程序转换为时间自动机模型FBDProgramModel()，如图5所示。

图5 程序模型FBDProgramModel()

程序模型可以描述为：

其中，FBExecuteModel()是PLC循环执行模型。

目前，使用Uppaal检测工具来验证时间自动机，该工具利用一组有界整型变量的时间自动机，模拟非确定性并行过程的实时系统。Uppaal的时序逻辑（TCLT）使用路径公式量化模型的路径及轨迹[9]。需要验证的标准如下：系统可达性、是否存在死锁情况、系统在y轴上的运行距离不能超过抛球机实物的轴长度800。所使用的性质验证语句如下所示：

P1：E＜＞ fbd.End；模型可达性验证。

P2：E＜＞ FBEN.End；模型可达性验证。

P3：A[] not deadlock；模型死锁情况验证。

P4：A[] Position_Y＜800；模型安全性验证，系统在y轴上的运行距离不能超过抛球机实物的轴长度800。

在Uppaal系统验证器中分别输入以上的验证语句，验证结果如图6所示。其中满足E＜＞ fbd.End和E＜＞FBEN.End性质表示该模型的可达性满足，说明存在路径开始于初始状态并最终满足模型的结束状态，验证该系统能顺利执行完成，功能块程序能到达最终状态。死锁状态是指这个状态和它的延迟后续没有任何输出动作，性质A[] not deadlock验证结果为满足，表示该系统在任何状态下不存在死锁，即该模型的状态都可以有输出动作。性质A[] Position_Y＜800验证模型的安全性，验证结果为满足，表示Position_Y＜800在可达状态下永远为真。验证结果表明满足验证的全部性质，即验证了程序的可靠性。

图6 验证情况

4 结语

本文致力于对PLCopen标准运动控制功能块图程序进行建模及验证，功能块图语言采用图形化描述，结构简单并且易于实现复杂的控制程序，是运用最为广泛的PLC标准编程语言。经过深入分析国内外现状和查阅大量有关文献，本文实现了将功能块转换为时间自动机，利用Uppaal检测工具验证其可达性、死锁、安全性等性质，从而可以对程序进行可靠性验证。通过实验结果，开发人员可以发现程序或系统的安全性问题或性能改进点，从而更好地改进系统。