基于PLC建模的正式检查方法

基于PLC建模的正式检查方法摘文 高可靠性是电气控制设备的关键性能。PLC是结合了计算机技术、自动控制技术和通信技术,被广泛用于工业过程的自动化技术。在本文中,提出了一个有效的方法用于PLC系统的建模和验证。为了确保PLC的高速特性,我们提出了一个“时间间隔模型”技术和“notice-waiting”。它可以降低状态空间,也可以验证一些复杂的PLC系统。同时,从PLC构建模型转换Promela语言来获得建模和检查工具PLC-Checker的PLC系统设计。尽管PLC这种逻辑错误发生的概率非常小,但是发生错误可能导致系统崩溃。接下来使用PLC-Checker检查一个古典PLC的例子,这是一个反例。关键词:模型检查、PLC建模、PLC-Checker正式的方法1. 介绍 1 PLC是一种自动控制装置,可以从传感器接收信息,计算设备或其它PLC逻辑输入信号和输出信号的逻辑处理。可以使用标准语言编写控制算法,如梯形图(LD)、结构化的文本(ST)或指令表(IL)。 2 使用PLC技术的可编程语言来控制大规模集成电路已广泛应用于工业。关于关键软件的安全可以严重危害生命或财产,验证关键软件的安全已经成为不可或缺的步骤，所以需要保证软件质量。目前的PLC验证方法仍是通过仿真和测试。然而,他们不能涵盖所有可能的情况下,特殊的PLC的设计模型是否满足需求。因此,模型检测技术引入PLC的领域。提供给PLC设计重要的理论分析。 3 PLC模型检测的主要步骤是建立PLC模式,如建立模型函数图表。4关于PLC模型建立的时间属性。它可以被建模的方法有时间自动机5或时间段建模方法6。7 因此状态空间模型与时间自动机相比将下降。不管怎样选择,最终都可以抽象模型。对于如何构建一个好的PLC抽象模型检查是最重要的问题。手动建模很容易引入许多错误,所以建立一个集成建模和测试工具是非常重要的,这是本文关注的问题之一。 PLC控制程序在实时操作系统中运行(多任务或单一任务);本文主要是基于多任务调度PLC系统。第二节的文章介绍了PLC系统的建模方法。第三节给出了此模型的分析和改进,还有我们需要减少虚拟错误的概率。第四节是设计一个模型检测工具PLC-Checker检查建立模型,包括介绍了PLC程序转换成主要的输入语言Promela的代码。最后，介绍了一个应用PLC-Checker检查和一个关键问题的经典例子。2. PLC建模 有三个步骤的模型检查:建模、属性描述和验证。最重要的是如何构建系统模型。 在系统中,PLC控制器不是孤立的,而是由驱动程序和人控制它的工作环境8。因此,这些因素也应该被建模。环境、人、PLC控制器是相互独立和并发的逻辑。同时,模型检查器转换的输入语言Promela侧重于描述并发,所以从这个观点中,我们建立这些因素分成几个并发进程转换符合检查,它也会准确地描述这个系统。为了描述方便,他们将被称为并发实体。PLC控制器与并发交互实体通过符号表来表示。PLC系统的符号包括I(输入端)、Q(输出端口)和M(中间继电器)。图1是一个图表的PLC系统模型。 时间间隔建模策略:使用特定的并发实体的一些特定的状态代表了并发中的实体状态,而不考虑系统时钟。这可能忽视特定的时差,从而简化了PLC模式。建模策略不添加系统时钟属性,不能完全符合最初的PLC模式。主要是由于加入系统时钟会引起PLC系统模型太大,没有模型检查工具来处理如此大的模型。建模的起点状态是不考虑PLC迁移时扫描的数量有经验。不管经历了多少扫描,他们都将包括在这个模型。换句话说,真正的模型将是建立模型的一个子集(时间间隔模型)。 PLC的现实环境是复杂的,包括各种硬件和人为的行为。下面我们将分析不同类型的PLC并发实体环境。1) 硬件实体 硬件实体的PLC中,PLC控制系统主要是一些设备。这些设备的状态可以输入PLC控制器。虽然硬件都有自己的工作流程,但这个流程是由硬件需求决定的。因此,绑定硬件实体及其相关I和Q,。这个工作流程可以抽象为自动机。该自动机用于描述硬件的工作状态。 定义2.1.一个硬件实体是一个元组Env = , I env是I的端口绑定与硬件实体，Q env是Q的端口绑定的实体。A是自动机描述实体的工作流程，A是一个元组 A = ,当s 0的初始状态是A，S是特定集合T的转移。 硬件实体的状态是I的一个子集符号,和标志每个状态都映射到真,假,I没有出现的特定状态可以是真或假(即:任意行动)。硬件实体的转移与Q的子集直接表达符号表示所有问符号子集是真实的同时将驱动状态之间的迁移。硬件实体的状态转换图还需要从这个状态转换图指定一个初始状态。 硬件实体的状态转换图是基于分工的象征,不考虑时间和属性。硬件实体状态转换图实际上是一个忽略时间的抽象硬件实体,且需要抽象模拟硬件的参考。2) 简单输出实体 简单的输出实体只有绑定Q端口不使用I端口，这意味着简单输出实体没有状态转换图。简单的输出实体显示了PLC的工作状态的设备,像一个信号光。使用简单的输出实体是绑定的Q端口,PLC可使其进行逻辑设计。M端口Q端口I端口PLC控制器扫描和计算设置端口的值 并发的实体简单的输出实体硬件实体人类行为实体 图1所示 PLC系统模型 3) 人类行为的实体 定义2.2.人类行为的实体是一个元组 Env= ,当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上升边检测器,底片边缘探测器下降等等。基本逻辑运算网络建模,我们使用直接映射方法,即:PLC控制器模型的网络行为和网络的逻辑行为是完全等价的。S触发器，R触发器，SR触发器，EQ触发器，RS触发器可以直接使用布尔表达式映射到他们的行为。3所示。PLC)模型的分析和改进 前一节中描述了PLC系统的建模,根据这一战略,我们可以抽象的把PLC系统作为一个正式的模型进行模型检查。因此,这个模型将直接决定模型检测结果的可信度。如果模型不完全覆盖原系统(我们称之为小于原系统),有可能会导致一些错误不会发现,如果模型可以完全覆盖真正的系统,但它包含许多状态,而原系统不存在(我们称之为比原系统大),这可能引入一些错误,则真正的系统不存在。在这里称之为误差。所以建模策略有两个要求。 首先,为了找到系统中所有的错误,我们将构建一个模型足以涵盖所有美国原始系统;其次,要求模型尽可能接近真实的系统。这不仅会降低状态空间,但也提高效率。基础上的需求,我们将给出一个分析时间间隔模型。 命题1如果时间间隔模型符合特性,也符合真正的PLC系统模型。 命题1的正确性可以从两个模型之间的关系得出的结论。这意味着所有的情况下,真正的模型会发生时间间隔,包括时间间隔模型。如果你不能找到一个反例来通过使用一个时间间隔模型,你可以证明真正的PLC模型的正确性;另一方面,如果我们找到一个反例,我们不能确定是否有真正的PLC系统中的错误。也就是说命题1的假设是错误的。然后需要手动干预分析反例确定误差。扫描m扫描1传输完成开始转移时间t 1t mt 0t m+ 并发的实体PLC控制器 PLC块 注意实体延续 图2。注意等待机制的并发实体。 时间间隔建模策略可以得到一个抽象的PLC模型,许多研究还根据使用NuSMV研究类似于时间间隔模型PLC模型系统。然而,“时间间隔模式”与真正的大偏差模型需要改善。偏差是:“时间间隔模式”并不能反映PLC的高速扫描特性和低速并发实体的特征。也就是说,所有的环境的变化应该由PLC高速扫描,但时间间隔模型忽略了PLC的高速特性,使外部环境的变化，可能不会被扫描。为了解决上述问题,考虑到外部高速扫描和低速并发物理特性，时间间隔建模策略通过添加注意等待机制完善。基于时间间隔模型,每个并发状态实体必须阻塞和等待后发生转移。只有在PLC控制器完全扫描至少一次,注意等待机制将消息发送给并发实体的块,然后才继续工作。完成转移后，并发的进程实体在注意等待机制下完成迁移工作如图2所示: t 0:转移开始,块,注意到PLC控制器。 1 t - t m:PLC完全扫描m(m至少一个）。 t m + 1:并发实体得到PLC的信号,完成转移。 这种机制确保了每一个状态改变的并发实体可以通过PLC控制器至少被扫描一次。 命题2添加注意等待机制后,该模型成为时间间隔模型的一个子集。同时,该模型还可以包括整个局势真正的模型。也就是说,如果一个模型添加注意等待机制符合特性,也符合真正的PLC系统模型。 它类似于证明命题与命题1 2。命题2中我们可以看到,在添加注意等待机制模型仍然具有良好的性质。正如前面提到的,一个抽象的系统模型有两个要求:首先,完全包含真正的系统,其次是模型尽可能接近真实系统。第一个命题证明的时间间隔模型包括真正的系统,只要使用模型检查工具来证明这个抽象模型满足一定的特性,然后系统的本质也会满足这个。但这模型和实际模型并不完全相同的情况下,它应该是远大于实际模型。与时间间隔模型相比,该模型进一步降低实际系统之间的距离,大大减少发生误差的机会。模型检测工具会给出一个破坏特性制度的反例;很容易手动确定反例在现实系统是真的还是假的。如果这一个反例是在原系统存在的错误。那么这个错误是因为在抽象模型中比真正的系统大,这是一个误差。因此,虽然这个时间间隔模型和原系统不完全相同,但是通过这个模型,我们可以判断一个系统满足一定的特性,如果不是我们可以找到一个特定的反例(仍然需要更多的研究来确定是否有误差)。 模型并不等同与原系统,主要是因为有许多因素难以模型在实际系统,其中一些可能会导致错误。如果所有的因素进行建模,这将导致建立一个巨大的模型,无法检查,或者根本无法实现。时间间隔模型抽象的关键因素从实际系统和模型,大大减少了状态空间,降低时间复杂度。注意等待机制的存在,使添加的模型变得更接近实际系统,不仅降低了时间复杂度,同时减少了之前提到的误差。4所示。PLC模型检查 PLC广泛应用在许多应用程序和很多设备中;这是一个大的研究领域。PLC任何的工作环境,都包括了不同的设备和人,所以PLC系统并发。同时,PLC系统很难找到如果有一些错误,主要是因为逻辑设计的错误,而不是计算误差。我们专注于PLC程序逻辑过程的检测,和这个逻辑可以完全由一些逻辑描述。因此,为了简化PLC程序模型,集中在模型检查,我们进行以下设置: PLC是一种逻辑控制程序,所有的控制变量只有0和1两种状态; 在并发环境中PLC程序运行。在这种情况下,PLC编程更可能有一些错误不容易找到。 具上述特点,我们使用模型检查工具转换(我们的工具PLC检测程序实现NuSMV)对上述建立的模型检查。我们做了一系列的转换规则,建立上述模型转换为输入语言Promela,系统属性也需要翻译成Promela,转换后将把它们放在一起,然后执行检测。 PROMELA语言是一个C类语言,它们在语义上是相似的。所以我们只会给一些例子显示翻译的基本概念。看到PROMELA语言的细节,请访问。我们将介绍三个PROMELA文件作为输入的一部分。1) PLC控制器的代码 PLC控制器是由多个网络组成的。PLC控制器的代码也是来自网络。当然,在那之前,你应该申报所需要的变量。每个网络都有其输入端口和输出端口,每个端口可以表明一个布尔表达式。我们分配输出端口的值通过计算逻辑的输入端口。这是PLC网络的翻译方法。 这是一个老转换网络的例子:if: Exp(R) = 1 - Q = 0;:else -if :Exp(S) = 1 - Q = 1;:else - skip; fi;fi;/ * Exp(S)是布尔表达式的港口Exp(R)是R的布尔表达式端口Q是输出端口* /2) 并发实体代码 我们认为每个并发实体一个独特的过程,不管它是人类行为或设备。这些过程与PLC控制器进程共享变量。必须这样做,以确保系统的并发性。在本文的第二部分,我们将讨论所有的并发实体建模为一个自动机。自动机的意思是从一个状态转移到另一个地方。我们使用I端口形成实体的状态。使用goto语句作为转移(就像在汇编语言)。一个简单的例子如所示:StateA:atomic if: Q1 - IB, goto StateB: Q2 - IC, goto StateCfi;/ * StateA状态的标签Q1、Q2是转移的条件IB是设置状态值状态B的值goto StateB意味着跳到StateB * /3) 代码的特性 特性是PLC系统必须遵守的规则。我们使用LTL(线性时间逻辑)公式的输入格式。我们应该写计数器属性的机制。转换会在一个我们特定的情况下发生,这应该是一个反例。我们不能直接写LTL公式,要通过使用宏。首先我们应该在一个宏定义所有命题LTL(如# define p i5 = = 0),然后使用LTL定义形成命题公式。SPIN可以自动转换LTL公式PROMELA代码通过使用“SPIN-f”指令(见更多的细节在SPIN手册)。4) 注意等待机制 在建模讨论,我们建议增加注意等待机制。这种机制也需要反映在代码。具体实现是为每个non-PLC签署一些变量的过程(所有流程PLC控制器除外)作为一个信号。自动机状态转移标签时,信号变量设置为0,和下一个任务需要1继续这个变量。PROMELA语法特性的结果,过程将挂起。PLC过程中没有这样的限制,相反,PLC过程可能将这些变量设置为1,从而确保每一个动作必须经过至少一个PLC扫描完成。这就是所谓的注意等待机制。 遵循以上四个步骤,我们得到一个完整的代码的SPIN系统的输入文件。然后我们可以使用SPIN检查模型。SPIN模型检查器的操作步骤,看SPIN的手册(请访问)。SPIN结果是否找到反例,我们可以使用上述理论分析SPIN的跟踪文件。 使用这种检测机制,我们开发了一个工具检查PLC检测程序模型。它有助于构建可视化模型和实施检查,并可以给一个简单的分析结果。当然,相反的例子,找到应用手动检查以确定是否真正的反例。然而,在小径的帮助文件,这不是一个非常困难的任务。我们还成功地实现一些检查使用PLC检测程序。在一个典型的范例,找到了一个反例。虽然反例的发生概率很低,但它确实发生,可能造成严重后果。这个工具也证明了本文理论的正确性和有效性。5。运行PLC检测程序 我们将介绍PLC的有效性检查器通过检查一辆双门通道模型。双门通道用于防止一个封闭的房间与外界联系。 通过输入梯克和并发实体工具,在符合属性的定义下,我们执行检查。图3显示了结果。 我们可以看到,有一个错误的结果。它被证实是一个真正的反例通过检查手动跟踪文件。也就是说我们的机制是有效的检查这样的PLC程序。6。结论 我们研究的理论建模和检查PLC系统在正式的方法。PLC建模分析的要求,和并发实体的模型是建立在时间间隔的方法。然后我们证明的时间间隔模型一套超级的PLC系统,通过添加注意等待机制和减少模型。这也保证了考试的所有更改可以扫描系统中PLC控制器。我们发现系统的误差通过检查系统的反例。最后,用SPIN的方式检查模型。也对相应的模型检查工具PLC-Checker介绍。在这个阶段,机制仍然有许多缺陷,如处理定时器。但它在解决问题的探索有伟大的和独特的优点，表现我们仍在积极探索问题。引用1 Pavlovic, R. Pinger and M. Kollmann, “Automated Formal Verification of PLC Programs Written in IL,” Conference on Automated Deduction (CADE), Bremen, July2007, pp. 152-163.2 M. B. Younis and G. Frey, “Formalization of Existing PLC Programs: A Survey,” Proceedings of CESA 2003,Lille, 2003.3 N. Bauer, S. Engell, S. Lohmann, M. Remelhe and O.Stursberg, “Verification of PLC Program Given as Sequential Function Charts,” Lecture Notes in Computer Science, Vol. 3147, 2004, pp. 517-540.4 S. R. Koo, P. H. Seong and S. D. Chaa, “Software Design Specification and Analysis Technique for the Safety Critical Software based on Programmable Logic Controller (PLC),” Proceedings of the Eighth IEEE International Symposium on High Assurance Systems Engineering (HASE04), Florida, March