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: / 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 (like # define p i5 == 0), then we use propositions defined to form a LTL formula. SPIN can automatically convert the LTL formula to PROMELA code by using “SPIN–f” instruction (see more details in manual of SPIN). 4) Notice-waiting mechanism
In the modeling discussion, we propose to add notice-waiting mechanism. Thismechanism also needs reflected in the code. Specific implementation is to sign a bit variable for each non-PLC process (all the process except PLC controller) as a signal. When the automata transfer to a state label, the signal variable is set to 0, and the next assignment requires this variable to be 1 to continue. As the result of PROMELA grammatical features, the process will hang onwards. In the PLC process no such restrictions, on the contrary, PLC process can set these variables to 1, thus ensuring every move must go through at least one PLC scan to complete. That is the so called notice-waiting mechanism. Follow the four steps above; we get a complete code of a SPIN input file of our system. Then we can use SPIN to check the model. For the steps of operating SPIN model checker, see the manual of SPIN (visit www.spinroot.com). SPIN will give the result whether a counter- example is found, and we can analyze using the theory mentioned above with the trail files that spin gives. Using this detection mechanism, we developed a tool for model checking PLC-checker. It helps to build visual models and the implementation of checking, and can give a simple analysis to the result. Of course, the counter-example it find should be checked manually to make sure whether it is a true counter-example. However,
64
with the help of trail file, this is not a very difficult task. We also successfully implemented some checking using PLC-checker (shown in the next section). In a classic textbook example, a counter-example was found. Although the probability of occurrence of counter-example is very low, but it does happen and can have serious consequences. This tool is alsoproves the correctness and validity of the theory in this article.
5. Running PLC-Checker
We will show the effectiveness of PLC checker by checking a two-door channel model. A two-door channel is used to prevent a closed room from the contact with the outside world. into the tool, also the definition of the property, we execute thechecking. Figure 3shows the result. As we can see, there is one error in the result. It is proved to be a true counter-example by checking the trail file manually. That is to say our mechanism is effective in checking such kind of PLC programs. 6. Conclusions
We study the theory of modeling and checking on PLC system in formal method in this paper. The requirement of PLC modeling is analyzed, and the models ofconcurrent entities are built up through time interval strategy. Then we prove the time interval model a super set of the PLC system, and decrease the model by adding notice-waiting mechanism. It alsoensures all the changes in the system can be scanned by the PLC controller. We find the error of the system by checking out the counter-example of the system. Finally, the way of using SPIN to check the model is given. Also the corresponding model checking tool PLC-Checkeris introduced. In this stage, the mechanism still has many imperfections, such as the handling of the timer. But it has great and unique advantages in solving the problem of state exploration. We are still on active exploration of such issues.
65
REFERENCES
[1] Pavlovic, R. Pinger and M.Kollmann, “Automated Formal Verification of PLC Programs Written in IL,” Conference on Automated Deduction (CADE), Bremen, July 2007, 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 HASE’04), Florida, March 2004, pp. 283-284. [5] A. Mader and H. Wupper, “Timed Automaton Models for Simple Programmable Logic Controllers,” Proceedings of the 11thEuromicro Conference on Real-Time Systems1999, York, June 1999, pp.106-113.
[6] E. Brinksma1, A. Mader and A. Fehnker, “Verification and Optimization of a PLC Control Schedule,” International Journal on Software Tools for Technology Transfer (STTT), Vol. 4, No. 1, October 2002, pp. 21-33.
[7] S. Lamp′eri`ere and J. J. Lesage, “Formal Verification of the Sequential Part of PLC Programs,” 5th Workshop on Discrete Event Systems (WODES2000), Ghent, August 2000, pp. 247-254.
[8] S. Kowalewski, S. Engell, J.Preu?ig and O. Stursberg, “Verification of Logic Controllers for Continuous Plants Using Timed Condition/Event-System Models,” Automatica: Special Issue on Hybrid Systems, Vol. 35, No. 3, March 1999, pp. 505-518.
66
PLC的建模与形式化检查已方法
摘要
高可靠性的关键是电气控制设备的性能。 PLC综合了计算机技术，自动控制技术和通信技术，并成为广泛用于工业过程的自动化。复杂的PLC系统的一些要求不能由传统的验证方式支付。在这种纸，对PLC系统的建模和验证的有效方法被提出。为了保证PLC的高速性能，我们提出了“时间间隔模式”和“通知等待”的技术。它可以减少状态空间并使其能够验证某些复杂的PLC系统。另外，从内置PLC型号为Promela语言的语言转换得到与工具PLC-检查员进行建模和checkingPLC系统的设计。运用PLC-检查器检查一个经典的PLC例子，一个反例被发现。虽然这个逻辑错误的发生概率非常小，它可能会导致系统崩溃致命的。
关键词：模型检验，模型的PLC，PLC的检查，形式化方法
1引言
PLC是，可以从传感器接收的信息的自动控制设备，计算设备或其他可编程控制器逻辑输入信号，并输出逻辑信号进行处理。控制算法可以使用标准的语言，如梯形图（LD ），结构化文本写入（ ST），或指令列表（IL ） [ 1 ]。可编程控制器采用可编程语言的技巧控制大规模集成电路已经广泛应用于在行业[ 2 ]。因为安全关键软件的可造成生命或财产，核实严重损害安全关键软件已经成为一个必不可少的步骤保证软件质量要求。本校验方法为PLC仍停留通过仿真和测试。但是，他们不能涵盖所有可能的情况下，特殊PLC的设计模型是否满足需求。因此，模型检测科技推出进入PLC领域要givetheoretical PLC的分析设计变得重要。PLC的模型检测的主要步骤是建立PLC型号，如树立样板从功能图[ 3 ]。 PLC型号集中在成立时属性[ 4 ]。它可以建模按时间自动机的方法[5]或时间段建模方法[ 6 ]。因此，模型的状态空间将减少了与时间自动机。无论哪种途径之一选择，最终的抽象模型可以得到[ 7 ]。如何建立一个良好的PLC的抽象模型是最重要的问题的检查。由于手工建模容易引入许多错误，所以建立一个集成的建模和测试工具是非常重要的，这也是关注本文的问题之一。PLC控制程序的实时操作系统（多任务还是单任务）运行;本文主要是基于上的多任务调度的PLC系统。的第2节文章有介绍的建模方法PLC系统。第3节给出了该模型的分析和改进，因为我们需要降低的可能性伪错误。第四部分设计了一个模型检测工具PLC-检查器检查所建立的模型，包括引进转化PLC程序到SPIN的方式输入语言Promela语言代码。最后，一个经典的PLC例如被施加到检查和临界弧段，例如由PLC ，检查发现。
67
2，PLC建模
有三个步骤模型检验的：造型，道具，PLC的建模与形式化方法1055检查已ERTY描述和验证。最重要的是如何建立系统模型。在系统中， PLC控制器不是分离的，而是具有其工作环境，司机和人类交互[8]。因此，这些因素也应该建模。环境，人类和PLC控制器是独立的，并发的相互逻辑。此外，该模型检测工具SPIN的输入语言Promela语言是专注在描述并发，所以从这个思路出发，我们建立这些因素分成几个并发进程适合从SPIN的检查，它也将准确地描述系统。为了描述方便，他们将所谓并发实体。 PLC控制器与互动通过在图像表中的符号并发实体。PLC系统的符号包括I（输入端口） ，Q（输出端口）和M （中间继电器） 。图1是一个图中的PLC系统模型。时间间隔建模策略：用国旗哪些特定的并发实体的位状态表示并行实体的状态，而不考虑到系统时钟。这可能会忽略时间国家的差异，从而简化了PLC型号。该建模策略不会将系统时钟性质，不完全对应与原来的PLC模型。这主要是由于加入了系统时钟会导致PLC系统模型变得过大，不存在为模型检测工具来处理这么大的模型。起点造型像状态 这是不是要考虑PLC的扫描次数，当迁移是经验丰富。不管有多少扫描它经验丰富，他们都将包括在这个模型。在换句话说，真实模型将是内置的一个子集模型（时间间隔模型） 。真正的PLC环境是复杂的，并且包括一各种硬件和人类行为。下面我们会给不同种类的PLC环境的并发实体的分析。 1 ）硬件实体
PLC系统的硬件实体主要是一些设备的PLC控制。这些设备的状态可以是PLC控制器的输入端。因此，本与其相关联的I和Q ，硬件实体结合而硬件都有自己的工作流程，这个流程是通过对硬件的要求决定。这个工作流程可以被抽象成自动机。该自动机是用来描述硬件的工作状态。定义2.1 。 A硬件实体是一个元组包膜= < Ienv，Qenv ， A> ，其中Ienv与硬件的I端口绑定实体， Qenv与该实体在Q端口绑定。 A是自动机描述实体的工作流程， A是元组A =
68