外文文献翻译-基于形式化方法的PLC建模和检测【中文6440字】 【中英文WORD】

外文文献翻译-基于形式化方法的PLC建模和检测【中文6440字】 【中英文WORD】,中文6440字,中英文WORD,外文文献翻译-基于形式化方法的PLC建模和检测【中文6440字】,【中英文WORD】,外文,文献,翻译,基于,形式化,方法,PLC,建模,检测,中文,6440,中英文,WORD J.软件工程与应用，2010年，3，1054-1059 doi:10.4236/jsea.2010.311124网上公布2010年11月（http://www.SciRP.org/journal/jsea）版权所有 基于形式化方法的PLC建模和检测 郑岳山1,2，罗贵明1,2，孙俊波1,2，张俊杰1,2，王振峰1,2 1清华大学信息科学与技术国家重点实验室，清华大学，北京，中国；2软件学院，清华大学，北京大学，中国。 邮箱：championkop@gmail.com, gluo@tsinghua.edu.cn 2010年9月5日，2010年9月16日修订，2010年9月24日。 摘要 高可靠性是电气控制设备的关键性能。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检测发现一个重要的反例。 2. PLC建模 模型检测的三个步骤：建模，属性描述和验证。最重要的是如何建立系统模型。 在系统中，PLC控制器不是孤立的，而是受其工作环境，驱动程序和人类行为的影响[8]。因此，这些因素也应考虑到建模中来。环境，人和PLC控制器是独立的，并在逻辑上相互并行。此外，模型检测工具SPIN的输入语言PROMELA重点是描述并发系统的，所以从这个想法出发，我们建立几个并发机构，来运用SPIN工具，它也将准确地描述系统。为了描述方便，它们将被称为并发的实体。PLC控制器通过映像表中的符号与并发实体联系。PLC系统的符号包括I（输入端口），Q（输出端口）和M（中间继电器）。图1是PLC系统模型示意图。 时间间隔建模策略：使用特定位状态的并发实体的标志，代表并发实体的状态下，不考虑到系统时钟，忽视状态的时间差，从而简化了PLC建模。建模策略不添加系统时钟的属性，不完全对应与原PLC模型。这主要是由于加入系统时钟将导致PLC系统模型变得过于庞大，没有任何模型检测工具来处理这么大的模型。时间间隔建模的是以PLC在扫描时不考虑迁移量为起点情况下使用的。不管经历多少扫描都将包括在此模型中。换言之，真正的模型是所建模型（时间间隔模型）的一个子集。 真正的PLC环境是复杂的，包括了各种硬件和人类行为。下面我们将分析各种不同的PLC环境中的并发实体。 图1：PLC系统模型 1)硬件机构 PLC系统的硬件实体，主要是一些PLC控制设备。这些设备的状态可以作为PLC控制器的输入。因此，硬件实体与其相关的输入端口和输出端口相结合，并且拥有自己的工作流程，该工作流程是由所需硬件自身决定。这个工作流程可以抽象认为成是自动机，此自动机通常用来来描述的硬件的工作状态。 定义2.1。硬件实体是一个元组ENV = ，，其中Ienv是输入端口（I）绑定的硬件实体，Qenv是与实体结合的输出端口（Q）。 A是自动机用来描述实体的工作流程，A是一个元组A = ，其中S0是初始状态，S是状态的集合，而T是一系列的转换。 硬件实体的状态是符号I的一个子集，I标志着每个状态都映射为{真，假}，符号I不会出现既是真又是假（即：独断专行）。硬件实体的转变直接表达为符号Q的子集，也就是说在子集中所有符号Q同时都是真时，将推动状态与状态之间的迁移。硬件实体的状态转换图，还需要指定一个初始状态，转换图从这种状态。 硬件实体的状态转换图是基于符号I的划分，并没有考虑到时间属性。硬件实体状态转移图中被忽略的硬件实体的时间实际上是抽象的，这种抽象是硬件仿真所需的参考。 2)简单的输出机构 简单的输出实体结合的Q端口不使用I端口，这意味着简单的输出实体不具有的状态转变图。简单的输出实体是显示PLC工作状态的显示装置，就像一个光信号。简单的输出实体的与Q端口连接，因此PLC能对Q端口进行逻辑设计。 3)人的行为机构 定义2.2人的行为机构是一个元组ENV = ，其中Ienv 是I端口绑定的硬件实体，Qenv量是Q端口绑定的实体， A是自动机描述实体的工作流程，A是一个元组A = ，其中S0是初始状态，S是状态的集合，而T是一系列的转变。 人的行为机构与硬件机构类似，它们具有相同的状态定义。模拟人的行为是很困难的，尤其是一些涉及人的行为的PLC设计。针对这些困难，人的行为建模应采取一个反复的过程：首先，使用模型验证建立一个简单的行为模型，然后，如果没有找到一个反例子，则建立更复杂的模型并进行验证，直到找到一个反例或几乎不能再复杂为止；最后，如果前面没有找到有意义的反例，则生成一个完全随机的人的行为模式（即：所有转让是真实的人类行为是一个完整的图形）来核查。然而，完全随机行为的核查将导致状态空间的显着增加，因此如何选择一个合适的人类行为模式在建模中是存在很大难度的。如果人的输入比较简单，我们可以使用完全随机的行为建模，否则，你需要认真考虑建立一个理性的人的行为模式。 上面我们建立了PLC的环境和人的行为模型，然后我们将模拟PLC的控制器。当打开PLC控制器，。 •PLC读取I端口的所有输入。 •PLC计算所有的逻辑单元。 •PLC设置所有的Q端口。 PLC运行的基本单位称为网络。根据设计时设定的编码，所有的网络开始运行。PLC控制器基本逻辑运算网络包括：S触发器，R触发器，SR触发器，EQ触发器，RS触发器，POS上升沿检测器，NEG下降沿检测器等。要运行网络建模的基本逻辑，我们采用直接映射方法即：PLC控制器的网络行为和逻辑网络行为模式是完全等价的。其中S触发器，R触发器，SR触发器，EQ触发，RS触发器可以直接使用布尔表达式进行触发。 3.PLC模型的分析与改进 上一节介绍了PLC系统的建模，根据此策略我们可以抽象出一个PLC系统作为正式模型的检测模型。因此，这模式将直接决定模型检验结果的公信力。如果此模型不完全覆盖原来的系统（我们称之为小于原始系统），有可能会导致一些错误无法检测出来；如果真正的系统模型可被完全地覆盖，但其中包含了许多原系统不存在的状况（我们称之为大于原来的系统），这可能会引入真正的系统不存在的错误，我们把其称为伪错误。因此有两个建模的要求。 首先，为了找到系统中的所有错误，我们将建立一个模型，大到足以覆盖原系统的所有状态。第二，要求模型尽可能接近真实系统，这不仅会减少的状态空间，还能提高工作效率。基于要求，我们将给出一个关于时间间隔模型的分析。 命题1，如果时间间隔模型符合性能，真正的PLC系统模型也符合。 从两个模型之间的关系可以得出命题1的正确性结论。这意味着现实模型中会发生的所有的情况由时间间隔模型所包括，时间间隔模型是大于实际的模型。如果你不能用时间间隔模型找到一个反例，那你就可以证明真正的PLC模型的正确性;另一方面，如果我们找到一个反例，但无法确定PLC系统中是否真的存在此错误，也就是说逆命题是错误的。然后，需要手动干预分析此反例，以确定它是否是一个伪误差。 时间间隔建模策略可以得到一个抽象的PLC模型，基于对NuSMV的许多研究也可使用类似的时间间隔模型策略来建立PLC系统。然而“时间间隔模型”与真实模型有较大的偏差，从而需要加以改进。偏差是指：“时间间隔模式”并不能反映PLC在并发系统的高速扫描特性和低速特性。也就是说，所有环境的变化应由PLC快速的扫描，而时间间隔模型忽略了PLC的快速特性，这使得在外部环境的变化可能无法扫描。 为了解决上述问题，考虑到外部高速扫描和低速并发的物理特性，时间间隔建模策略应通过加入的通知等待机制来改善。在时间间隔模型的基础上，在发生传输后每个并发状态机构将被阻止并且等待。只有当PLC控制器至少完全扫描一次后，通知等待机制将发送的信息给机构移除阻止并继续工作，然后传输完成。通过并发机构的通知等待机制来完成传输的过程，如图2所示： 图2：并发系统的通知等待机构 •T0：传输开始，阻止并通知PLC控制器。 •T1-TM：PLC完全扫描m次（m为至少一个）。 •TM+1：并发机制从PLC中得到指令，传输完成。 这种机制确保每个并发机构状态的变化都能由PLC控制器至少一次扫描。 命题2：添加通知等候机制后，模型成为时间间隔模型的一个子集。同时，该模型也可以包括在现实模型中的所有情况，也就是说如果模型添加的通知等候机制符合属性，真正的PLC系统模型也符合。 这类似于命题1证明与命题2，我们可以看出添加等待通知机制后的模式仍具有良好的性质。正如前面提到的，抽象的系统模型有两个要求：第一，要充分包含真正的系统模型接近真实系统；其次，第一命题证明的时间间隔模型包括了真实的系统，只要使用模型检测工具证明这种抽象模型满足一定属性，那么原系统也将满足这一点。但这种模式和实际的模型是不完全等价的，它应该远远大于实际的模型。比较时间间隔模型，此模型与实际系统之间的距离将进一步减小，大大降低了找出伪错误的机会。 模型检测工具将给出一个违反系统属性的反例；在实际系统中很容易确定反例的真假。如果原系统中的错误真的存在，那么我们就找出一个反例。否则，该错误会由于抽象模型大于真实的系统，而成为一个伪误差。因此，虽然这个时间间隔模型和原来的系统是不能完全等同的，但通过这个模型我们可以判断系统是否符合一定的属性，如果不是我们可以找到一个具体的反例（仍需要更多的研究以确定它是否是一个伪误差）。 模型是不等于原系统的，主要是因为在实际系统中有许多因素难以模型，其中有一些可能会引起错误。如果所有的因素都为蓝本，将导致建立一个巨大的不可检测或根本无法实现的模型。时间间隔模型是从真正的系统和他们的模型中抽象出来的，可大大减少状态空间和时间复杂度。同时，添加通知等候机制，模型变得更接近真实系统，不仅降低了时间复杂度，同时减少了前面提到的伪错误。 4.PLC模型检测 PLC被广泛的使​​用在许多领域，并有丰富的品种，这是一个很大的研究领域。任何PLC工作在包括不同的设备和人员的环境中，所以PLC系统是并发的。如果出现误差，PLC系统很难在同一时间找到错误的所在，其中主要是因为逻辑设计错误，但不会产生的计算误差。所以我们专注于PLC程序的逻辑过程的检测，这个逻辑可以完全通过为逻辑来描述。因此，为了简化PLC程序模型，专注于模型检测，我们做如下设置： •PLC逻辑控制程序，所有的控制变量只有两个状态0和1; •PLC程序并发的环境中运行。在这种情况下，PLC编程更可能会有一些不容易发现的错误。 就上述特点，我们使用的模型检测工具SPIN（我们的PLC检查工具也识别NuSMV）对上述建立的模型进行检测。我们制定了一系列的转变规则，用SPIN的输入语言PROMELA建立上述模型中，系统属性也需要被翻译成PROMELA语句，SPIN将会把它们放在一起，然后进行检测。 PROMELA语言是一种C类语言，它们在语义上相似。所以我们将只举几个例子来展示翻译的基本概念。要详细了解PROMELA语言，请访问www.spinroot.com 我们将介绍作为SPIK输入的一个PROMELA文件的三个部分。 1）PLC控制器守则 PLC控制器由多个网络组成的， PLC控制器代码也从网络中产生。当然在这之前，应先声明所需的变量。每个网络都有它的输入端口和输出端口，每个端口可以用一个布尔表达式。我们通过逻辑运算来设计所有的输入端口输出端口的分配值,这是PLC网络的翻译方法。 下面是一个转变为SR网络的例子： if :: Exp(R) == 1 -> Q = 0; ::else -> if ::Exp(S) == 1 -> Q = 1; ::else -> skip; fi; fi; /* Exp（S）是S端口的布尔表达式 Exp（R）是R端口的布尔表达式 Q是输出端口*/ 2）并发机构守则 我们认为每个并发机构是一个独特的过程，不管是人的行为或设备。这些过程共享变量与PLC控制器的过程。这就确保了系统的并发性。 在本文的第二部分中，我们讨论所有并发机构的建模作为自动机。自动机的意思是从一个状态转变到另一个。我们使用的I端口形成的机构状态，使用goto语句作为转变语句（就像汇编语言）。一个简单的例子如下所示: StateA: atomic { if :: Q1 -> {IB, goto StateB} :: Q2 -> {IC, goto StateC} fi;} /*StateA的状态A的标志 Q1，Q2是转换条件 IB是所设置的到达状态B的价 goto StateB意味跳转到状态B*/ 3）属性守则 属性是PLC系统必须遵守的规则。我们使用LTL（线性时间逻辑）公式作为输入方式。由于SPIK的机制，我们应该编写反属性。SPIN将找出其属性在什么情况下发生，此状况则是一个反例。 我们不能直接写LTL公式，但使用宏指令。首先，我们应该用宏指令定义所有的LKL命题（例如定义p i5 == 0），然后我们用定义的命题，形成一个LTL公式。通过使用“SPIN-F”指令，SPIN可以自动转换LTL公式的PROMELA代码。 4)通知等候机制 在建模的讨论中，我们提出了添加通知等候机制。这种机制还需要在代码中反映出来，具体做法是确定每个非PLC过程（PLC控制器除外）的位变量，将其作为一个信号。自动机转换到状态标签时，设置的信号变量为0，直到下一个变量到来时变为1，否则继续保持为0。PROMELA语法结果的特点，是此过程将保存起来。而在在PLC过程中则没有这样的限制，相反，PLC过程可以设置这些变量为1，从而确保每一动作都必须经过至少一个PLC的扫描完成。这就是所谓的等待通知机制。 遵循上述四个步骤，我们得到了一个完整的SPIN输入文件代码，然后我们就可以使用SPIK来检测模型。对于SPIK模型检测器的运行步骤，请参阅SPIK的使用手册（访问www.spinroot.com）。SPIK能给出结果是否是所找的反例，而我们可以通过使用跟踪文件的方法得出上述结论。 使用这种检测机制，我们开发了一个能建模检测PLC模型的工具。它有助于建立可视化模型和实施检测，并且可以举出一个简单的分析结果。当然，发现反例则需要手动检测，以确保它是否是一个真正的反例，然而，有了跟踪文件的帮助使这成了一个并不困难的任务。我们还成功的采用了一些PLC检测（在下一节中所示）。教科书中发现的一个经典例子可做反例。虽然发生反例的概率是很低的，但它确实存在，并且可能会产生严重的后果。文章中此工具也证明了理论的正确性和有效性。 5.运行PLC检查 通过检测双门通道模型，来展示PLC检测的有效性。双门通道是通过一个封闭的空间来防止与外界的接触。 我们通过输入梯形图，并发机构工具和定义属性来执行检测。如图3所示结果 图3：模型检测结果 正如我们所看到的：是一个错误的结果，而且事实证明这是一个真正的通过手动检测跟踪文件得出的反例，也就是说我们的PLC程序检测这种机制是有效的。 6.结论 本文是研究的理论建模和检测PLC系统的优化方法。对PLC建模的要求进行了分析，并同过时间间隔策略建立起并发系统。然后，我们证明了时间间隔模式的PLC系统中的一个超集，并加入通知等候机制来降低了模型。通知等候机制还确保在系统中的所有的变化可以被PLC控制器扫描，并且我们找到了系统误差检测的反例，最后给出使用SPIK检测模型的方式。此外，引入了相应的模型检测工具PLC检测器。在此阶段，该机制仍然有许多缺陷，如定时器的处理，但它在解决空间探索问题上有很大而独特的优势。我们仍在积极的探索此类问题。 9 指导教师意见 指导教师签字： 年 月 日