plc正式的建模和检查的方法

学号10463331常州大学毕业设计（论文）外文翻译（2010届）外文题目PLCMODELINGANDCHECKINGBASEDONFORMALMETHOD译文题目PLC的正式建模和检查方法外文出处SCIENTIFICRESEARCH学院怀德学院专业班级电气101二一三年十一月目录摘要11介绍12PLC建模13PLC模型的分析和改进34PLC模型检查55运行PLC检查66结论7参考7摘要高可靠性是电气控制设备的关键性能。PLC结合计算机技术，自动控制技术和通信技术，并广泛应用于工业过程的自动化。一些需求复杂PLC的系统不能满足传统的验证方法。在本文中，提出了一个有效的PLC系统建模和验证方法。为了保证PLC的高速性能，我们提出了“时间间隔模式”和“通知等待”的技术。它可以减少状态空间并可以验证一些复杂的PLC系统。同时，通过建立PLC模型到PROMELA语言转换，用于建模和检查的PLC系统被设计出来了PLC检查器工具。使用PLC检查器核实一个经典的PLC的例子，发现一个反例。虽然这一逻辑错误发生的概率很小，这可能导致系统崩溃的致命的。关键词模型检查，PLC建模，PLC检查器，形式化方法1介绍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节给出了该模型分析和改进以及我们可以减少伪错误的可能。文章第4节设计的模型检测工具的PLC检查器检查所建立的模型，包括介绍PLC程序转换成SPIN的PROMELA代码输入语言的方法。最后是核实PLC的一个经典例子和PLC检查器发现的一个关键的反例。2PLC建模建模的步骤有三个模型、属性描述和验证。最重要的是如何构建系统模型。在系统中，PLC控制器不是孤立的，而是有其工作环境、驱动和本性的相互作用8。因此，这些因素也应该被建模。环境、本性和PLC控制器是独立和在逻辑彼此同时发生。同时，模型检查器SPIN的输入语言PROMELA集中描述同时发生，所以从这一思想出发，建立了这些多个并发进程因素来适应SPIN的检查，也将准确地描述系统。为了描述方便，它们将被称为并发实体。PLC控制器与并发实体通过符号图像表相互作用。PLC系统的符号包括I（输入端口），Q（输出端口），和M（中间继电器）。图1为PLC系统模型。图1PLC系统模型时间间隔的建模策略使用特定的并发实体的位状态的标志代表并发实体的状态，而不考虑系统时钟。这可以忽视状态的时间差，从而简化了PLC模型。建模的策略，没有增加的系统时钟性能，不完全符合原PLC的模型。这主要是由于加入的系统时钟将使PLC系统模型变得太大，没有模型检测工具来处理如此大规模的模型。像这样状态的建模出发点转移经历时是不考虑PLC次数扫描的。不管有多少次的扫描经历，它们都将包括在这个模型中。换句话说，实体模型是所建模型的一个子集（时间间隔模型）。真正的PLC环境是复杂的，包括各种硬件和人类行为。以下我们将提供不同种类PLC环境下的并行实体分析。1）硬件实体PLC系统的硬件实体主要是一些PLC控制的设备。这些设备的状态可以是PLC控制器的输入。因此，硬件实体和相关的I和Q的结合，而硬件有自己的工作流程，工作流程是由硬件要求决定。这个工作流程可以抽象成自动机。该自动机是用来描述硬件的工作状态。这个工作流程可以抽象成自动机。该自动机是用来描述硬件的工作状态。定义21硬件实体的一个数组是ENV，IENV的输入口和硬件实体是连接的，QENV的输出口和实体连接。A是自动机描述实体的工作流程，A的数组A，S0是初始状态的A，S是状态的集合，T是传输的集合。硬件实体的状态是符号I的子集，每个状态I信号都会映射到真，假，I的符号没有在状态出现可以是真也可以是假（即独断独行）。用符号Q的子集直接表达硬件实体的转移，所有在子集中的符号Q在同一时间的状态之间的迁移是真的。硬件实体的状态转换图还需要指定一个初始状态，转换图起始于这种状态。硬件实体的状态转换图是基于不同部门的符号I并且时间性质不作考虑。硬件实体的状态转换图实际上是忽略了时间的硬件实体抽象，这种抽象的模拟需要用硬件做参考。2）简单的输出实体简单的输出实体只与Q端口绑定而不使用I端口，这意味着简单输出实体没有状态转换图。简单的输出是实体显示PLC的工作状态的设备，如信号灯。简单的输出实体用法是和Q端口绑定，PLC可实现其逻辑设计。3）人类行为实体定义22人类的行为实体的一个数组是ENV，IENV的输入口和硬件实体是连接的，QENV的输出口和实体连接。A是自动机描述实体的工作流程，A的数组A，S0是初始状态的A，S是状态的集合，T是传输的集合。人类行为实体与硬件实体类似；它们有相同的状态定义。模拟人的行为是很难的，特别是一些涉及个人的PLC设计。针对这些困难，人类行为建模需要一个重复的过程首先，使用模型验证建立一个简单的行为模型；其次，如果没能找到一个反例，建立一个更复杂的模型并验证，直到找到一个反例或难以更复杂；最后，如果没有找到一个有意义的反例，就生成一个完全随机的个人行为模型（即人类的行为是一个完整的图形的所有传输是真的）来验证。然而，完全随机的行为验证将导致状态空间急剧增加，因此如何选择一个合适的人类行为模型在建模中是最有难度的。如果个人的输入是相对简单的，我们可以用完全随机的行为来建模，否则，你需要认真考虑建立一个合理的人类行为模型。我们将建立高于PLC环境和人类行为的模型，然后我们还将建立PLC控制器的模型。PLC控制器在打开时将在一个循环过程。PLC从I端口读取所有的输入。PLC计算所有的逻辑单元。PLC设置所有的Q端口。PLC的基本单元过程称为网络。所有的网络操作在设计时的根据是数字集合。PLC控制器的基本逻辑操作网络包括S触发器，R触发器，SR置“1”置“0”触发器，EQ触发器，RS置“0”置“1”触发器，POS上升边缘检测器，NEG下降边缘检测器等等。基本的逻辑操作网络建模，我们使用了直接映射策略，即网络行为的PLC控制器模型和网络的逻辑的行为是完全等价的。其中S触发器，R触发器，SR触发器，EQ触发器，RS触发器可以直接使用布尔表达式（BOOLEANEXPRESSIONS）来映射到它们的行为。3PLC模型的分析和改进前一部分介绍了PLC系统的建模，根据这一策略；我们可以抽象PLC系统为模型检验的形式化模型。因此,该模型将直接决定模型检测结果的可信度。如果模型没有完全覆盖原系统（我们称之为比原始系统小），则有可能导致一些没有被检测到错误；在真实系统中模型可以完全被覆盖，但它包含着原始系统不存在的状态（我们称之为比原始系统大），这可能会引入一些实际的系统中不存在的错误。在这里称之为伪错误。所以有两个建模策略的要求。首先，为了找到系统中所有的错误，我们将建立一个足以囊括所有原始系统状态的模型；其次，要求模型是尽可能的接近真实系统。这不仅可以减少状态空间，而且提高效率。基于此要求，我们将提供有关的时间间隔模型的分析。命题1如果时间间隔模型符合该属性，也符合真实的PLC系统模型。命题1的正确性可以从两个模型之间的关系得出结论。这意味着所有的情况下，实体模型将发生的事包括时间间隔模型，时间间隔模型比实体模型大。如果你不能通过使用一个时间间隔模型找到一个相反的例子，可以证明真正PLC模型的正确性；另一方面，如果我们找到了一个相反的例子，我们就不能确定是否是真实PLC系统的错误。也就是说命题1的逆命题是错误的。然后需要人工干预来分析反例，以确定它是否是一个伪错误。时间间隔建模策略可以得到一个抽象的PLC模型，许多基于NUSMV的研究也使用类似的时间间隔模型策略到PLC系统的模型。然而，“时间间隔模型”与实体模型有较大的偏差，需要改进。偏差就是“时间间隔模型”不能反映PLC的高速扫描特性和并发实体的低速特性。环境中的所有变化应该被PLC高速扫描，但时间间隔模型忽略了PLC的高速特性，这使得在外部环境的变化可能没被扫描。为了解决上述问题，考虑到外部高速扫描和低速并行的物理特性，时间间隔的建模策略应加注意通知等待机制的改进。在时间间隔模型的基础上，每一个并发状态的实体必须阻止，等待后才发生转移。只有当PLC控制器至少完成一次扫描，通知等待机制将发送至并发实体移除障碍，然后继续工作。然后，转移完成。并发实体工作的通知等待机制转移过程如图2所示图2并发实体通知等待机制T0转移开始，块和通知PLC控制器。T1TMPLC完全扫描M次（M至少是一次）。TM1并发实体从PLC得到通知，转移完成。这种机制确保并发实体每一状态的变化可以被PLC控制器至少扫描一次。命题2添加通知等待机制后，模型成为时间间隔模型的一个子集。同时，该模型还可以包括实体模型的整个情况。也就是说，如果一个模型添加的通知等待机制符合这种特性，真正的PLC系统模型也符合。命题2的证明和命题1类似。由命题2我们可以看到，添加了通知等待机制的模型仍具有良好的性质。正如前面提到的，一个抽象的系统模型有两个要求首先，充分包含真实的系统，其次是模型尽可能接近真实的系统。第一个命题证明的时间间隔模型包括真实的系统，只要使用模型检测工具来证明该抽象模型满足一定的特性，那么系统的本质也将满足这一点。但该模型和实体模型并不完全相等，应该远远大于实体模型。比较时间间隔模型，该模型进一步降低真实系统之间的距离，进而大大减少找到伪错误的机会。模型检查工具会给出一个反例违反的系统性能；它易于手动确定反例在真实的系统中是不是真的。如果原系统中的错误真的存在，那么我们找到一个反例。否则，这个错误是因为抽象模型大于真实的系统，这是一个伪错误。因此，虽然这个时间间隔模型与原系统不是完全等同的，但通过这种模型，我们可以断定一个系统满足一定的特性，如果没有，我们可以找到一个特定的反例（还需要更多的研究来确定它是否是一个伪错误）。模型不等于与原系统，主要是因为有许多因素在真实的系统中难以模仿，其中的一些可能会加大错误。如果所有的因素都进行建模，这将导致建立起一个巨大的模型以至于无法检查，或根本无法实现的。时间间隔模型抽象的关键因素是真实的系统和模仿他们，这大大减少了状态空间，并降低了时间复杂度。同时，通过添加通知等待机制，模型变得更接近真实的系统，不仅降低了时间复杂度，同时减少之前提到的伪错误。4PLC模型检查PLC被广泛运用于许多应用中，并且有许多设备；这是研究的一个大型领域。任何PLC的工作环境包括不同的设备和人员，所以PLC系统是并行。在同一时间，很难找到是否有一些错误，这主要是因为在逻辑设计错误，并不是计算错误。我们专注于PLC程序的逻辑过程的检测，这种逻辑可以通过位逻辑完全描述。因此，为了简化PLC程序模型，专注于模型检查，我们进行如下设置PLC是一种逻辑控制程序，所有的控制变量只有0和1两种状态；在并发环境中运行PLC程序。在这种情况下，PLC编程更可能产生一些错误不容易找到。在上述特征方面，我们利用模型检测工具SPIN（我们的PLC检查器工具实现了NUSMV）对已建立的上述模型进行检测。我们做了一系列的转换规则，建立了上述模型转化为SPIN的输入语言PROMELA，系统属性也需要被翻译成PROMELA语言，SPIN将它们放在一起，然后进行检测。PROMELA语言是C类的语言，它们在语义相似。所以我们只会给一些例子说明翻译的基本概念。看PROMELA语言的详情，请浏览WWWSPINROOTCOM。我们将介绍PROMELA文件的三个部分作为SPIN的输入。1）PLC控制器代码PLC控制器由多个网络组成。PLC控制器代码也从网络上产生的。当然，在这之前，你需要声明所需的变量。每个网络都有其输入端口和输出端口，每个端口可以表示的布尔表达式（BOOLEANEXPRESSION）。我们通过对所有输入端口的逻辑运算指定输出端口的值。这是PLC网络的翻译方法。这里是SR网络的转换例子IFEXPR1Q0ELSEIFEXPS1Q1ELSESKIPFIFI/EXPS布尔表达式表达式的S端口EXPR布尔表达式表达式的R端口Q输出端口/2）并发实体编码我们考虑每个并发实体的一种独特过程，无论是人类的行为还是设备。这些进程与PLC控制器进程共享变量。这是必须的以确保该系统的并发性。在本文的第二部分，我们讨论了所有的并发实体都作为自动机进行建模。自动机的意思是从一个状态转移到另一个状态。我们使用I端口以形成实体的状态。使用GOTO语句作为传输（就像汇编语言一样）。一个简单的例子是显示在下面STATEAATOMICIFQ1IB,GOTOSTATEBQ2IC,GOTOSTATECFI/STATEA是STATEA的标签Q1,Q2是转移条件IB是将状态值设置到状态B的值GOTOSTATEB意味着跳转至STATEB/3）编码的属性属性是PLC系统必须遵守的规则。我们使用的LTL（线性时间逻辑）公式作为输入格式。我们应该写反属性因为有SPIN机制。SPIN会发现一个我们属性发生的情况，这应该是一个反例。我们不能直接写LTL公式，但使用宏。首先我们应该在宏中LTL定义所有的命题LIKEDEFINEPI50，然后我们使用命题定义，形成一个LTL公式。SPIN可以通过使用“SPINF”指令PROMELA代码自动转换为LTL公式（更多详情见SPIN手动操作）。4）通知等待机制在建模的探讨中，我们提出了添加通知等待机制。这种机制也需要在代码中体现。具体的实施是为每个非PLC过程签署一个位变量（除了PLC控制器的所有进程）作为一种信号。当自动机转移到状态标签，信号变量被设置为0，接下来的任务需要此变量为1以继续。由于PROMELA语法特征的结果，这个过程将挂起。PLC过程中没有这样的限制，相反，PLC程序可以设置这些变量为1，从而确保每一个动作都必须经过完成至少一次PLC扫描。这就是所谓的通知等待机制。按照以上四步；我们得到了一个完整的SPIN输入文件的系统代码。然后我们可以使用SPIN检查模型。操作SPIN模型检查器的步骤，请查看SPIN手动操作（访问WWWSPINROOTCOM）。SPIN给出的反例是否找到的结果，我们可以分析使用前面提到的理论来追踪SPIN给出的文件。利用该检测机制，我们开发了一种用于模型检查的PLC检测器。它有助于建立视觉模型和执行情况检查，并可以给一个简单的分析的结果。当然，反例发现后应再用手动检查以确定它是否是一个真正的反例。然而，在跟踪文件的帮助下，这也不是一个非常困难的任务。我们还成功地实现了利用PLC检测器一些检查（在下一节中所示）。在经典范例中找到了一个反例。虽然反例发生的概率是非常低的，但它确实发生了，并且产生严重的后果。这个工具也证明了本文理论的正确性和有效性。5运行PLC检查我们将通过检查两门通道模型显示PLC检测器的效力。两门通道用于防止封闭的房间里和外面的世界接触。通过输入梯图（响度平衡）和并发实体成为工具，同时定义属性，我们执行检查。图3显示结果。图3模型检查结果我们可以看到，有一个错误的结果。这证明检查手动跟踪文件是一个真正的反例。这也就是说我们这种检查PLC程序的机制是有效。6结论我们在此文中研究了在PLC系统的正式建模和检测方法理论。我们对PLC建模的要求进行分析，并发实体的模型通过时间间隔策略已经建立。然后，我们证明了时间间隔模型的一个超集PLC系统，并通过添加通知等待机制降低模型。它还确保系统中所有的变化都可以通过PLC控制器扫描。我们通过检查系统的反例发现系统错误。最后，使用SPIN验证给出的模型。还介绍了相应模型的检测工具PLC检查器。在此阶段，该机制仍然有许多缺陷，如定时器的处理。但它在解决状态探索问题方面有着良好的和独特的优势。我们仍在积极探索这种问题。参考1PAVLOVIC,RPINGERANDMKOLLMANN,“AUTOMATEDFORMALVERIFICATIONOFPLCPROGRAMSWRITTENINIL,”CONFERENCEONAUTOMATEDDEDUCTIONCADE,BREMEN,JULY2007,PP1521632MBYOUNISANDGFREY,“FORMALIZATIONOFEXISTINGPLCPROGRAMSASURVEY,”PROCEEDINGSOFCESA2003,LILLE,20033NBAUER,SENGELL,SLOHMANN,MREMELHEANDOSTURSBERG,“VERIFICATIONOFPLCPROGRAMGIVENASSEQUENTIALFUNCTIONCHARTS,”LECTURENOTESINCOMPUTERSCIENCE,VOL3147,2004,PP5175404SRKOO,PHSEONGANDSDCHAA,“SOFTWAREDESIGNSPECIFICATIONANDANALYSISTECHNIQUEFORTHESAFETYCRITICALSOFT