检验和优化一个PLC控制时间表

中文字数: 2066,中文页数: 3  英文字数:  1958 ,字符数:10360  ,页数:5

检验和优化一个PLC控制时间表
Edmund Brinksma1，AngelikaMader1,Ansgar Fehnker2
1计算机科学的天才，特湾特大学,荷兰;发电子邮件给: {brinksma,mader}@cs.utwente.nl
2电子和计算机工程学，卡内基美隆大学,美国;电子邮件:ansgar@ece.cmu.edu
在线出版:2002.10.2
摘要：
我们报道为最完整的过程控制程序和最佳的时间表提供检查技术的模板使用。大多数的这个工作是为欧盟VHS计划(混合的系统)实行,如一个案件的研究部份，在那个计划对化学工厂的实验中的一个可控制逻辑控制器(PLC)来说，必须被正确设计。我们最初的意图是要看有多少可以在这里使用标准的模型检查环境。随着即时的样板检验员的检测，其代价可能是相当昂贵。依我们的情况,我们用抽象化技术处理了PLC控制器。对于流程安排我们实现一个叫做变数中时间优先的方案，比较且解释我们在外面的相同案件研究，由于样板检验员的帮助, 证明了提高设备对查证控制器的设计及在合理时间上对最佳的时间表需求是有力的。
关键字:正式的方法–模型检查–混合的系统–行程安排

Verification and optimization of a PLC control schedule
Ed Brinksma1, AngelikaMader1, Ansgar Fehnker2
1Faculty of Computer Science, University of Twente, Netherlands; E-mail: {brinksma,mader}@cs.utwente.nl
2 Electrical & Computer Engineering, Carnegie Mellon University, USA; E-mail:
Published online: 2 October 2002 –   Springer-Verlag 2002
Abstract:
We report on the use of model checking techniques for both the verification of a process control program and the derivation of optimal control schedules. Most of this work has been carried out as part of a case study for the EU VHS project (Verification of Hybrid Systems), in which the program for a Programmable Logic Controller (PLC) of an experimental chemical plant had to be designed and verified. The original intention of our approach was to see how much could be achieved here using the standard model checking environment of SPIN/Promela. As the symbolic calculations of real-time model checkers can be quite expensive it is interesting to try and exploit the efficiency of established non-real-time model checkers like SPIN in those cases where promising work-arounds seem to exist. In our case we handled the relevant real-time properties of the PLC controller using a time-abstraction technique; for the scheduling we implemented in Promela a so called variable time advance procedure. To compare and interpret the results we carried out the same case study with the aid of the real-time model checker UPPAAL, enhanced with facilities for cost-guided state space exploration. Both approaches proved sufficiently powerful to verify the design of the controller and/or derive (time-) optimal schedules within reasonable time and space requirements.
Keywords: Formal methods – Verification – Model checking – Hybrid systems – Scheduling

相关论文