基于FSM的PLCopen运动控制系统可靠性研究

何 洁，李 贤，高 健

(1.杭州电子科技大学 计算机学院，浙江 杭州 310018；2.北京百度网讯科技有限公司，北京 100193)

PLCopen(PLC)标准的运动控制功能块是基于IEC61131-3标准定义的一组功能块语言，因其采用统一接口以提高代码复用性和系统可重构性的特点而被多数厂商青睐[1-2]。安全工业系统的开发对PLC软件的安全性要求越来越高[3]，工程师需要在实施应用之前对系统进行可靠性验证。

目前国内外学者针对PLC系统的可靠性分析进行了大量研究，并取得了一定的成果。文献[5]通过自动生成面向单元的测试例，分析系统可靠性，但是无法准确定位出错位置。文献[6]提出了基于Petri网结构描述各单元之间的逻辑结构，通过实例比较了Petri网与传统梯形图之间的优势和不足。文献[7]将PLC程序的Petri网模型和计算树逻辑(CTL)输入模型检测工具NuSVM，进行程序验证。文献[8]将PLC系统等价描述为SMV模型验证器语言，实现了简单系统的安全验证，但是由于检测方法的限制，该方法并不适用复杂系统。文献[9]使用时间自动机模型描述功能块(FBD)系统，将描述的自动机模型转化为NuSVM语言。文献[10]和文献[11]将PLCopen标准的SFB程序和IEC61131标准FBD程序使用时间自动机形式化语言描述，使用UPPAAL模型验证器验证PLC系统可靠性，该方法适用于实时系统。以上模型转换时均采用直接转换，但是由系统到模型转换过程复杂，不易发现转换错误。

本研究分析了PLCopen标准运动控制系统以及功能块之间转换关系，将PLCopen运动控制系统通过时间自动机建模进行描述并使用UPPAAL模型验证器加以验证。本研究为PLCopen标准的运动控制系统安全性提供了理论支持；同时提出了自动机分层描述系统思想，降低状态之间的耦合度，减少了系统到模型转换的出错率。

1 PLCopen标准运动控制

PLCopen运动控制功能块是由国际PLCopen组织提出的一种采用统一接口的功能块语言，被用于提高代码复用性和可移植性[12]。PLCopen运动控制功能块分为三部分：参数、功能块名称、内部算法。参数部分又包含输入参数、输出参数和输入输出参数。

PLCopen标准根据功能分为两大类：管理类和运动类。管理类功能块主要是读取运动状态以及运动参数信息等；运动控制类功能块则负责控制轴速度、位移等。本文研究的是基本控制即主从关系的运动系统[13-14]，其可被划分为8种基本状态{Homing，StandStill，Disable，ErrorStop，Stoping，Discrete Motion，Continue Motion，Synchronized Motion}，分别为置位、停滞状态、失能状态、错误停止、停止、离散运动、连续运动、同步运动。各种状态之间可以相互转换，如图1所示。

2 PLCopen运动控制系统建模

首先对PLCopen的8种运动状态使用时间自动机形式化语言进行建模，模型为系统主模型。为减少状态之间的耦合度，研究中引入SB(StandBy)虚节点，将运动状态部分分层处理。随后对PLCopen标准的系统程序建立时间自动机模型，将模型转化为UPPAAL验证工具语言，在验证工具中多层次(系统程序模型、系统主模型和运动状态模型)执行程序。最后对输出结果进行验证，验证流程如图2所示。

图1 PLCopen标准基本状态图

图2 验证流程

2.1 UPPAAL的时间自动机定义

UPPAAL由Aalborg大学和Uppsala大学于1995年联合提出[15-16]，是进行系统建模和验证的工具，适用于描述非确定性实时系统。

2.2 PLCopen运动控制系统建模

系统主模型有8种基本状态分别为：SM(SynchronizedMotion)、DM(DiscreteMotion)、 CM(ContinuousMotionstate)、SP(Stoping)、ES(ErrorStop)、HM(Homing)、SS(Standstill), DS(Disabled)。为降低8种状态之间的耦合度，文章引入SB状态，SB状态是虚拟状态节点，系统由其它状态进入SM、CM或DM时，应首先进入SB状态。引入SB可以更好的建立运动控制模型，减少状态之间的复杂度。

PLCopen运动控制时间自动机系统主模型(MCA)定义如下：，L=Lstate是系统的轴状态，Lstate={SM,DM,CM,SP,ES,HM,SS,DS,SB}表示轴的9种状态集合，Laxis={Axisx,Axisy,Axisz…}表示系统中所包含的轴，如表示某一轴的一个状态；L0={< DS,Axisn>,Axisn∈Laxis}是系统的初始状态；E⊂L×Φ×Σ×2C×L，E表示一个转换集合，其中Σ=Σ1×Σ2是自动机的输入集，Σ1={memory unit}，Σ2={READ,WRITE}定义为对内存的操作；I是l到l′的映射记做∈E；LF是模型定义的系统目标域，是一个有序状态集，与系统模型的执行序列进行匹配。图3(a)所示是由UPPAAL中所构建成功的以单轴为例的主系统模型，以DS为初始状态。图3(b)所示是分离的运动状态模型，由SB虚拟节点开始。

图3 系统主模型与运动状态模型

系统主模型初始状态为< DS,Axisn>，DSToSSConditoin是DS到SS的映射条件，当系统输入E(DSToSSConditoin (axis))=true时DS->SS跳转成功。DSToSSUpdate是更新变量。运动状态模型由开始，，和是执行状态。MCA适用于任何PLCopen运动控制系统验证，当系统主模型建立完成之后，对具体运动控制系统程序使用时间自动机进行形式化描述(具体系统具体分析)，运动控制系统进行验证时对系统程序模型和MCA同时执行UPPAAL验证。

3 实例介绍

列举货物运输系统进行实例说明，系统根据指令运动指定位移后返回，以单轴为例对其简化描述。图4是货物运输系统的一段核心程序，本文对其进行建模以分析系统可靠性。

图4 运输系统程序

系统完成的功能是上电、置位、移动规定步长、按规定速度移动、停止。首先分析系统结构特点，使用时间自动机形式化描述该系统PA定义如下：PA =；输入状态序列有PL={MCPower，MCHome，MCMoveRelative，MCMoveVelocity，MCStop }，初始状态PL0={start}，结束状态PLF={End}，PE=PL1×Φ×Σ×2C×PL2为状态间变换的边，是跳转的条件，详细定义见代码附录。

根据以上UPPAAL时间自动机形式化语言描述，对如上系统转换生成的UPPAAL系统模型如图5所示。

图5 系统程序模型

根据系统程序以及时间自动机形式化描述定义，转换生成UPPAAL中系统程序模型，其过程是将形式化定义解析转换成UPPAAL可解析的XML格式。黑色圆点所在的位置表示系统执行到的状态。系统主模型、系统运动状态模型和系统程序模型同时执行，不仅可以验证系统逻辑正确性，还可以检验程序XML到UPPAAL时间自动机XML转换的正确性。在UPPAAL工具中执行过程如图6所示

图6 运输系统检测结果

系统程序由Start进入上电状态。系统主模型中状态由DS进入SS，图中红色节点表示处于该节点状态。左侧模拟Trace窗口存储系统状态路径。下方窗口有p1，main和motion通道，分别表示系统程序、系统主状态、运动状态3条执行顺序。3种模型的完整状态路径如图7所示。

图7 运输系统状态输出路径

其中p1，main，motion的状态变化相互依赖，当p1由Start状态进入MCPower状态时，main进入SS，motion保持SB状态，以此类推，其路径时序以及状态变化正确即证明了系统逻辑是可靠的。

4 结束语

本文研究了PLCopen标准的运动控制系统可靠性验证模型，提出了通过时间自动机模型建模以及利用UPPAAL分析系统可靠性的新方法。该方法将系统程序模型与系统主模型分层描述，降低了状态之间耦合度，减少了模型转换过程的出错率。在下一步的研究中，研究者将专注于描述多并发和轴组关系的运动控制系统。