基于FSM的PLCopen运动控制系统可靠性研究
|
摘要
针对PLCopen运动控制系统安全验证问题,对PLCopen标准运动控制功能块语言、系统运动状态关系等方面进行了研究,提出一种新的分层描述时间自动机模型。该模型将系统程序状态与系统状态分别抽象定义,通过UPPAAL验证器进行验证,以状态路径正确或错误转换作为系统可靠的分析结果,从而实现系统的逻辑安全验证。实验结果证明该方法可以完成PLCopen标准运动控制系统的逻辑安全验证,并且有效减少了模型转换的出错率。
Aiming at the problem of security verification of PLCopen motion control system,a new hierarchical description time automaton model was proposed based on the study of PLCopen standard motion control function block language and system motion state relation. The model was used to define the system program state and the system state respectively. The UPPAAL validator was used to verify the system,and the logical path of the system was verified by the correct or wrong conversion to the state path. Experimental results showed that this method could complete the logic security verification of PLCopen standard motioned control system,and effectively reduce the error rate of model conversion error rate.
Aiming at the problem of security verification of PLCopen motion control system,a new hierarchical description time automaton model was proposed based on the study of PLCopen standard motion control function block language and system motion state relation. The model was used to define the system program state and the system state respectively. The UPPAAL validator was used to verify the system,and the logical path of the system was verified by the correct or wrong conversion to the state path. Experimental results showed that this method could complete the logic security verification of PLCopen standard motioned control system,and effectively reduce the error rate of model conversion error rate.
引文
[1] Thramboulidis K,Soliman D,Frey G. Towards an automated verification process for industrial safety applications[C]. Trieste:IEEE International Conference on Automation Science and Engineering,IEEE,2011.
[2]徐福生.基于PLCopen的视觉功能块的研究与实现[D].杭州:杭州电子科技大学,2016.
[3]齐鹏飞,罗继亮,陈雪琨.基于形式化方法的PLC程序设计与验证研究综述[C].厦门:过程控制会议,2012.
[4] Provost J,Roussel J M,Faure J M. Generation of single input change test sequences for conformance test of programmable logic controllers[J]. IEEE Transactions on Industrial Informatics,2014,10(3):1696-1704.
[5] Jamro M. POU-oriented unit testing of IEC 61131-3 control software[J]. IEEE Transactions on Industrial Informatics,2015,11(5):1119-1129.
[6]温世刚.基于Petri网的梯形图程序建模以及验证方法研究[D].厦门:华侨大学,2014.
[7] Estevez E,Marcos M. Model-based validation of industrial control systems[J]. IEEE Transactions on Industrial Informatics,2012,8(2):302-310.
[8] Yoo J,Cha S,Jee E. A verification framework for FBD based software in nuclear power plants[C]. Beijing:Asia-Pacific Software Engineering Conference, IEEE Computer Society,2008.
[9]李建龙. PLC系统及其FBD编程语言的形式化建模与实时性验证[D].厦门:华侨大学,2015.
[10]Soliman D,Frey G. Verification and validation of safety applications based on PLCopen safety function blocks[J]. Control Engineering Practice,2011,19(9):929-946.
[11]Soliman D,Thramboulidis K,Frey G. Transformation of function block diagrams to UPPAAL timed automata for the verification of safety applications[J]. Annual Reviews in Control,2012,36(2):338-345.
[12]罗林丹,包健. PLCopen运动模块参数传递方法的研究[J].机电工程,2014,31(7):945-950.
[13]田琦,李琪,姚鹏,等.基于模糊PID的全方位移动机器人运动控制[J].电子科技,2011,24(9):131-133.
[14]杨广泽,马晓明.串联机械臂运动控制系统设计[J].电子科技,2016,29(3):71-74.
[15]Mokadem H B,Berard B,Gourcuff V,et al. Verification of a timed multitask system with UPPAAL[J]. IEEE Transactions on Automation Science&Engineering,2010,7(4):921-932.
[16]周清雷,姬莉霞,王艳梅.基于UPPAAL的实时系统模型验证[J].计算机应用,2004,24(9):129-131.
[17]Enoiu E P,Sundmark D,Cˇau2evi c'A,et al. Mutation-based test generation for PLC embedded software using model checking[C]. Graz:IFIP International Conference on Testing Software and Systems,Springer International Publishing,2016.
[2]徐福生.基于PLCopen的视觉功能块的研究与实现[D].杭州:杭州电子科技大学,2016.
[3]齐鹏飞,罗继亮,陈雪琨.基于形式化方法的PLC程序设计与验证研究综述[C].厦门:过程控制会议,2012.
[4] Provost J,Roussel J M,Faure J M. Generation of single input change test sequences for conformance test of programmable logic controllers[J]. IEEE Transactions on Industrial Informatics,2014,10(3):1696-1704.
[5] Jamro M. POU-oriented unit testing of IEC 61131-3 control software[J]. IEEE Transactions on Industrial Informatics,2015,11(5):1119-1129.
[6]温世刚.基于Petri网的梯形图程序建模以及验证方法研究[D].厦门:华侨大学,2014.
[7] Estevez E,Marcos M. Model-based validation of industrial control systems[J]. IEEE Transactions on Industrial Informatics,2012,8(2):302-310.
[8] Yoo J,Cha S,Jee E. A verification framework for FBD based software in nuclear power plants[C]. Beijing:Asia-Pacific Software Engineering Conference, IEEE Computer Society,2008.
[9]李建龙. PLC系统及其FBD编程语言的形式化建模与实时性验证[D].厦门:华侨大学,2015.
[10]Soliman D,Frey G. Verification and validation of safety applications based on PLCopen safety function blocks[J]. Control Engineering Practice,2011,19(9):929-946.
[11]Soliman D,Thramboulidis K,Frey G. Transformation of function block diagrams to UPPAAL timed automata for the verification of safety applications[J]. Annual Reviews in Control,2012,36(2):338-345.
[12]罗林丹,包健. PLCopen运动模块参数传递方法的研究[J].机电工程,2014,31(7):945-950.
[13]田琦,李琪,姚鹏,等.基于模糊PID的全方位移动机器人运动控制[J].电子科技,2011,24(9):131-133.
[14]杨广泽,马晓明.串联机械臂运动控制系统设计[J].电子科技,2016,29(3):71-74.
[15]Mokadem H B,Berard B,Gourcuff V,et al. Verification of a timed multitask system with UPPAAL[J]. IEEE Transactions on Automation Science&Engineering,2010,7(4):921-932.
[16]周清雷,姬莉霞,王艳梅.基于UPPAAL的实时系统模型验证[J].计算机应用,2004,24(9):129-131.
[17]Enoiu E P,Sundmark D,Cˇau2evi c'A,et al. Mutation-based test generation for PLC embedded software using model checking[C]. Graz:IFIP International Conference on Testing Software and Systems,Springer International Publishing,2016.