外文文献翻译-基于形式化方法的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 指导教师意见 指导教师签字： 年 月 日 J. Software Engineering & Applications, 2010, 3, 1054-1059 doi:10.4236/jsea.2010.311124 Published Online November 2010 (http://www.SciRP.org/journal/jsea) Copyright PLC Modeling and Checking Based on Formal Method* Yueshan Zheng1,2, Guiming Luo1,2, Junbo Sun1,2, Junjie Zhang1,2, Zhenfeng Wang1,2 1Tsinghua National Laboratory for Information Science and Technology, Tsinghua University, Beijing, China; 2School of Software, Tsinghua University, Beijing, China. Email: championkop@gmail.com, gluo@tsinghua.edu.cn Received September 5th, 2010; revised September 16th, 2010; accepted September 24th, 2010. ABSTRACT High reliability is the key to performance of electrical control equipment. PLC combines computer technology, automatic control technology and communication technology and becomes widely used for automation of industrial processes. Some requirements of complex PLC systems cannot be satisfied by the traditional verification methods. In this paper, an efficient method for the PLC systems modeling and verification is proposed. To ensure the high-speed property of PLC, we proposed a technique of “Time interval model” and “notice-waiting”. It could reduce the state space and make it possible to verify some complex PLC systems. Also, the conversion from the built PLC model to the PROMAL language is obtained and a tool PLC-Checker for modeling and checking PLC systems are designed. Using PLC-Checker to check a classical PLC example, a counter-example is found. Although the probability of this logic error occurs very small, it could result in system crash fatally. Keywords: Model Checking, PLC Modeling, PLC-Checker, Formal Method 1. Introduction PLC is an automatic control device that can receive information from sensors, computing device or other PLC logic input signal, and output the logic signal processed. The control algorithm can be written using standard language, such as Ladder Diagram (LD), Structured Text (ST) or Instruction List (IL) [1]. The technique of PLC using programmable language to control large scale integrated circuit has been widely used in industry [2]. Because of safety critical software can cause serious damage to life or property, verification of safety critical software has become an indispensable step required to assure software quality. The present verifying method for the PLC is still stuck by simulation and testing. However, they cannot cover all possible cases, especial whether the design model of PLC to meet the demand. Therefore, the model checking technology is introduced into the field of PLC. To give theoretical analysis of PLC design becomes important. The primary step of PLC model checking is to the establishment of PLC model, such as establish a model from Function Charts [3]. The PLC model focuses on the establishment of the time attributes [4]. It can be modeled by the method of timed automata [5] or time period modeling method [6]. Thus state space of the model will be decreased compared to timed automata. Either way one choose, eventually an abstract model can be given [7]. How to build a good PLC abstract model is the most important issue to the checking. As the manually modeling is easy to introduce many errors, so the establishment of an integrated modeling and testing tool is very important, and this is one of the issues of concern to this paper. PLC control program runs in real-time operating sys-tem (multi-task or single-task); this paper is mainly based on multi-task scheduling PLC system. Section 2 of the article has an introduction to the modeling method of PLC system. Section 3 gives the analysis and improvement of this model as we need to reduce the probability of pseudo-errors. Section IV designs a model checking tool PLC-Checker to check the established model, including introduce the way of converting PLC program into SPIN's input language PROMELA code. Finally, a classical PLC example is applied to check and a critical counter-example is found by the PLC-Checker. 2. PLC Modeling There are three steps of model checking: modeling, property description, and verification. The most important is how to build the system model. In the system, PLC controller is not isolated, but has interaction with its working environment, driver and human [8]. Therefore, these factors should also be modeling. The environment, human, and the PLC controller is independent and concurrent with each other in logic. Also, the model checker SPIN’s input language PROMELA is focused on describing the concurrent, so starting from this idea, we build these factors into several concurrent processes to fit the checking from SPIN, it will also accurately describe the system. To describe conveniently, they will be called concurrent entities. PLC controller interacts with the concurrent entities through the symbols in image table. The symbols of PLC system include I (input port), Q (output port), and M (intermediate relay). Figure 1 is a diagram of PLC system model. Time interval modeling strategy: using the flag which specific the bit state of concurrent entities to represent the concurrent entities in the state, without regard to the system clock. This may neglect the time difference of states, thus simplifying the PLC model. The modeling strategy does not add the system clock properties, not fully corresponds with the original PLC model. That is mainly due to join the system clock will cause PLC system model become too large, there is no for model checking tool to deal with such a large model. The starting point for modeling the state like this is not to consider the number of PLC scans when a migration is experienced. No matter how many scans it experienced, they will all include in this model. In other words, the real model will be a subset of the built model (Time interval model). The real PLC environment is complex, and includes a variety of hardware and human behavior. The following we will give an analysis of different kinds of PLC environment concurrent entities 1) Hardware entity Hardware entity of the PLC system is mainly some equipment that PLC controls. The state of these equipments can be the input of PLC controller. Therefore, the hardware entity binding with its associated I and Q, while the hardware has its own workflow, this workflow is decided by the hardware requirements. This work flow can be abstracted into automata. This automata is used to describe the working status of the hardware. Definition 2.1. A Hardware entity is a tuple Env = , where Ienv is the I port binding with the hardware entity, Qenv is the Q port binding with the entity. A is the automata that describes the work flow of the entity, A is a tuple A = , where s0 is the initial state of A, S is the set of states while T is the set of the transfers. The states of hardware entities is a subset of I symbols, and the I’s sign each state are all mapped to {True, False}, the I symbol do not appear in the state can be either True or False (that is: act arbitrarily). The transfer of the hardware entities directly expressed with the subset of Q symbols, said that all Q symbols in the subset be true at the same time will drive migration between states. The state transition diagram of hardware entities also need to specify an initial state, the transitions graph starts from this state. The hardware entities’ states of transition diagram are based on the division of symbol I, and time properties are not taken into account. Hardware entities state transition diagram is actually an abstract of hardware entity ignored time, the abstract simulation required reference of the hardware. 2) Simple output entity Simple output entity only binding with the Q port without using I port, that means the simple output entities does not have a state transition diagram. Simple output entity is the equipment that shows the work state of PLC, like a signal light. The usage of the simple output entity is to bind with the Q port such that the PLC can make its logical design. 3) Human behavior entity Definition 2.2. A Human behavior entity is a tuple Env = < Ienv, A>, where Ienv is the I port binding with the hardware entity, Qenv is the Q port binding with the entity. A is the automata that describes the work flow of the entity, A is a tuple A = , where s0 is the initial state of A, S is the set of states while T is the set of the transfers. Human behavior entity is similar with Hardware entity; they have the same state definition. It is difficult to simulate the behavior of people, especially the design of a PLC to a number of individuals involved. In response to these difficulties, human behavior modeling should take an iterative process: First, a simple behavior model is built use the model validation; then, if not find a counter example, a more complex model is built, and validate, until find a counter-example or hard to be more complex; Finally, if not previously find a meaningful counter-ex-ample, then generate a completely random person behavior model (that is: human behavior is a complete graph with all transfers be true) to verification. However, completely random behavior’s verification will cause state space increases dramatically, so how to choose a suitable model of human behavior is the difficulty in modeling. If the person's input is relatively simple, we can use completely random behavior modeling, otherwise, you need to seriously consider the establishment of a rational model of human behavior. We build model to PLC environment and the human behaviors above, and then we will model the PLC controller. PLC controller will be in a loop when it is turned on. •PLC read all the input from I ports. •PLC compute all the logic units. •PLC set all the Q ports. PLC process on the basic unit called Network. All the networks will operate in order according to the number set when design. Basic logic operation network of PLC controller includes: S Trigger, R Trigger, SR flip-flop, EQ trigger, RS flip-flop, POS rising edge detector, NEG falling edge detector and so on. To the basic logic operation network modeling, we use direct mapping strategy, namely: PLC controller model of network behavior and the logical behavior of the network is completely equivalent. Where S trigger, R trigger, SR flip-flop, EQ trigger, RS flip-flop can directly use Boolean expressions to mapped to their behavior. 3. PLC Model’s Analysis and Improvement The previous section describes the modeling of a PLC system, according to this strategy; we can abstract a PLC system as a formal model for model checking. Therefore, this model will have a direct decision of the credibility of the model checking results. If the model does not fully cover the original system (we call smaller than the original system), there may cause some errors are not detected; model can be completely covered if the real system, but it contains many states that the original system does not exist (we call it larger than the original system), this may introduce some errors that real system do not exist. Here called it pseudo-error. So there are two requirements for modeling strategy. First, in order to find all the errors in the system, we shall build a model large enough to cover all the states in the original system; second, require the model be close to the real system as much as possible. This will not only reduce the state space, but also improve efficiency. Base on the requirements, we will give an analysis about the Time interval model. Proposition 1 If time interval model conforms the property, real PLC system model also conforms. The correctness of Proposition 1 can be concluded from the relationship between the two models. That means all the situations that real model will happen are included by the time interval model, time interval model is larger than the real model. If you couldn’t find a counter-example by using a time interval model, you can prove the correctness of the real PLC model; the other hand, if we find a counter-example, we cannot determine whether there are errors in the real PLC system. That is to say the converse of proposition 1 is wrong. Then manual intervention is required to analyze the anti-cases to determine whether it is a pseudo-error. Time interval modeling strategy can get an abstract PLC model, many research based on NuSMV also use the strategy similar to time interval model to model PLC system. However, the “time interval model” has large deviation with the real model, it needs to be improved. The deviation is: “time interval model” does not reflect the high-speed scanning characteristics of PLC and low-speed characteristics of concurrent entities. That is, all the changes in the environment should be scanned by the high-speed PLC, but the time interval model ignores the high-speed characteristics of PLC, which makes changes in the external environment may not be scanned. To address the above issues, taking into account the external high-speed scanning and low-speed concurrent physical characteristics, time interval modeling strategy shall be improved by adding a notice-waiting mechanism. Base on the time interval model, each concurrent state entity must be blocked and wait after the transfer took place. Only if the PLC controller completely scans at least once, the notice-waiting mechanism will sent messages to concurrent entities to remove the block and go on working. Then the transfer finished. The process that concurrent entities work to complete the migration by notice-waiting mechanism is shown in Figure 2: •t0: Transfer start, block and notice the PLC controller. •t1-tm: PLC completely scanned m times (m is one at least). •tm+1: The concurrent entities get the notice from the PLC, transfer finish. This mechanism ensures every state change of concurrent entities can be scanned at least once by PLC controller. Proposition 2 After add the notice-waiting mechanism, the model become a subset of the time interval model. At the same time, the model can also include the entire situation in real model. That is to say, if a model which adds the notice-waiting mechanism conforms the property, real PLC system model also conforms. It is similar to prove proposition 2 with proposition 1. By proposition 2 we can see, after add the notice-waiting mechanism the model still has a good nature. As previously mentioned, an abstract system model has two requirements: first, to fully contain the real system, followed by the model as close to real systems. The first proposition is proved that the time interval model includes the real systems, as long as the use of model checking tools to prove that this abstract model satisfies a certain property, then the true nature of the system will also satisfy this. But this model and the real model is not entirely equal, it should be far greater than the real model. Compare to time interval model, this model further reduced the distance between the real systems, greatly reduce the chance that finding out pseudo-errors. Model checking tool will give out a counter-example violate the property of the system; it is easy to manually determine the counter-examples in the real system is true or not. If the errors in the original system really exist, then we find a counter-example. Otherwise, this error is because the abstract model is larger than the real system, it is a pseudo-error. Therefore, although this time interval model and the original system are not fully equivalent, but by this model, we can judge a system meets a certain property, if not we can find a specific counter-example (still needs more examine to determine whether it is a pseudo-error). Model is not equivalent with the original system, mainly because there are many factors difficult to model in real systems, some of which may give rise to error. If all the factors are modeled, that will lead to the establishment of a huge model that cannot check, or simply cannot be achieved. Time interval model abstract the key factors from the real system and model them, greatly reducing the state space, and reduce the time complexity. Meanwhile, add by the notice-waiting mechanism, the model become much closer to real systems, not only reduces the time complexity, while it reduced the pseudo-errors mentioned before. 4. PLC Model Checking PLC is widely used in many applications, and has many devices; this is a large area of research. Any PLC work in the environment that includes different equipment and people, so PLC system is concurrent. At the same time, a PLC system difficult to find if there are some errors, mostly because of the logical design errors, but not the calculation error. So we focus on the detection of PLC program logic process, and this logic can be completely described by bit logic. Therefore, in order to simplify the PLC program model, focused on model checking, we make the following settings: •PLC is a logic control program, all the control variables only has two states 0 and 1; •PLC program is run in concurrent environment. In this case, PLC programming is more likely to have some errors not easy to find. In respect of the above characteristics, we use the model checking tool SPIN (our tools PLC-Checker also realized NuSMV) on the above established model for checking. We made a series of transformation rules, build the above model into SPIN's input language PROMELA, the system property also need to be translated into PROMELA, SPIN will put them together and then perform detection. PROMELA language is a C class language, they are similar in semantic. So we will only give some examples to show the basic concept of the translation. To see the details of PROMELA language, please visit www.spinroot.com. We will introduce the three part of a PROMELA file as the input of SPIN. 1) Code of PLC controller PLC controller is composed of multiple networks. Code of PLC controller is also generated from the network. Of course, before that, you should declare the variables you need. Each network has its input ports and output ports, each port can be indicate by a Boolean expression. We assign the output port’s value through the logic computing of all the input port. This is the translation approach of PLC network. Here is an example of converting SR network: if :: Exp(R) == 1 -> Q = 0; ::else -> if ::Exp(S) == 1 -> Q = 1; ::else -> skip; fi; fi; /* Exp(S) is the Boolean expression of S port Exp(R) is the Boolean expression of R port Q is the output port */ 2) Code of concurrent entities We consider each concurrent entity a unique process, no matter it is human behavior or equipment. These processes share variables with PLC controller process. This must be done to ensure the concurrency of the system. In the 2nd part of this paper, we discuss that all the concurrent entities are modeled as an automata. The meaning of automata is to transfer from a state to another. We use the I port to form the state of the entities. Use goto statement as the transfer (just like in Assembly language). A simple example is shown like below: StateA: atomic { if :: Q1 -> {IB, goto StateB} :: Q2 -> {IC, goto StateC} fi;} /* StateA is the label of State A Q1, Q2 is the condition of transfer IB is to set the state value to the value of state B goto StateB means jump to stateB */ 3) Code of property Property is the rule that the PLC system must obey. We use LTL (Linear Time Logic) formula as the input format. We should write the counter-property because of the mechanism of SPIN. SPIN will find a situation that our property happens, that should be a counter-example. We couldn’t directly write the LTL formula, but by using macros. Firstly we should define all the propositions in the LTL in a macro