参考文献/References:
[1] 吕卫阳.PLC技术综述[J].自动化博览,2008(增刊1):16-19.
[2] FREY G,LITZ L.Formal methods in PLC programming[C]//International Conference on Systems, Man and Cybernetics, Tennessee.Nashville:IEEE Press,2000:2431-2436.
[3] HOLLOWAY L E,KROGH B H.Synthesis of feedback logic for a class of controlled petri nets[J].IEEE Transaction on Automatic Control,1990,35(5):514-523.
[4] PELED D A.Software reliability methods[M].New York:Springer-Verlag,2001:1-9.
[5] BENDER D F,COMBEMALE B,CREGUT X,et al.Ladder metamodeling and PLC program validation through timed Petri nets[C]//4th European Conference on Model Driven Architecture-Foundations and Applications.Berlin:Springer,2008:121-136.
[6] 韩赞东,刘继国,罗晟.基于控制Petri网的高温气冷堆燃料装卸过程控制系统设计方法[J].核动力工程,2008,29(1):14-18.
[7] GIUA A,SEATZU C.Modeling and supervisory control of railway networks using Petri nets[J].IEEE Transaction on Automation Science and Engineering,2008,5(3):431-445.
[8] DURMUS M S,SOYLEMEZ M T.Railway signalization and interlocking design via automation Petri nets[C]//Proceedings of the 7th Asian Control Conference.Hong Kong:[s.n.],2009:1558-1569.
[9] 贾洋,肖武,董宏光.基于自组织Petri Net的间歇过程换热网络优化设计[J].化工学报,2010,61(12):3167-3171.
[10] 胡昌华,王青,陈新海.基于Petri网的导弹控制系统故障诊断梯形图求解法[J].宇航学报,2001,22(1):37-42.
[11] 大卫 R,奥兰 H.佩特利网和逻辑控制器图形表示工具(GRAFCET)[M].北京:机械工业出版社,1995:5-6.
[12] DU Yu-yue,JIANG Chang-jun,ZHOU Meng-chu.A Petri-net-based correctness analysis of internet stock trading systems[J].IEEE Transactions on Systems, Man and Cybernetics, Part C: Applications and Reviews,2008,38(1):93-99.
[13] VENKATESH K,ZHOU Meng-chu,CAUDILL R J.Comparing ladder logic diagrams and Petri nets for sequence controller design through a discrete manufacturing system[J].IEEE Transactions on Industrial Electronics,1994,41(6):611-618.
[14] HANISCH H M,THIEME J,LIIDER A,et al.Modeling of PLC behavior by means of timed net condition/event systems[C]//Proceedings of the 6th International Conference on Emerging Technologies and Factory Automation.Los Angeles:[s.n.],1997:391-396.
[15] KOTINI I,HASSAPIS,MODELING G.Performance evaluation of hybrid systems[C]//Proceedings of the 1st South-East European Workshop on Formal Methods.Thessaloniki:[s.n.],2003:21-35.
[16] FREY G,LITZ L.Correctness analysis of Petri net based logic controllers[C]//Proceedings of American Control Conference.Chicago:[s.n.],2000:3165-3166.
[17] FREY G,LITZ L.Analysis of Petri-net based control algorithms-based properties[C]//Proceedings of American Control Conference.Chicago:[s.n.],2000:3172-3176.
[18] FREY G,LITZ L.Automatic implementation of Petri net based control algorithms on PLC[C]//Proceedings of American Control Conference.Chicago:[s.n.],2000:2819-2823.
[19] WANG Rui,SONG Xiao-yu,ZHU Jian-zhong,et al.Formal modeling and synthesis of programmable logic controllers[J].Computer in Industry,2010,61(1):23-31.
[20] ALUR R,DILL D L.A theory of timed automata[J].Theoretical Computer Science,1994,26(2):183-235.
[21] PERME T.Translation of extended Petri net model into ladder diagram and simulation with PLC[J].Strojniski vestnik-Journal of Mechanical Engineering,2009,55(10):608-622.
[22] DIDEBAN A, KIANI M, ALLA H.Implementing PN-based controller with mutually exclusive transitions by SFC[C]//Proceedings of the 35th IEEE Annual Conference of Industrial Electronics.Porto:[s.n.],2009:4353-4358.
[23] TAHOLAKIAN A,HALES W M M.PNP?PLC: A methodology for designing, simulating and coding PLC based control systems using Petri nets[J].International Journal of Production Research,1997,35(6):1743-1762.
[24] JONES A H,UZAM M,KHAN A H,et al.A general methodology for converting Petri nets into ladder logic: The TPLL methodology[C]//Proceedings of the 5th Internatioal Conference on Computer Integrated Manufacturing and Automation Technology.Grenoble:[s.n.],1996:357-362.
[25] 琚长江,杨根科.Petri网在模块化制造系统PLC程序设计中的应用[J].低压电器,2006(4):20-23.
[26] LEE G B,HAN Z D,LEE J S.Automatic generation of ladder diagram with control Petri net[J].Journal of Intelligent Manufacturing,2004,15(2):245-252.
[27] WIGHTKIN N,BUY U,DARABI H.Formal modeling of sequential function charts with time Petri nets[J].IEEE Transactions on Control System Technology,2011,19(2):455-464.
[28] BEHRMANN G,DAVID A,LARSEN K G.A tutorial on uppaal[J].Lecture Notes in Computer Science,2004,3185:33-35.
[29] MOKADEM H B,BÉRARD B,GOURCUFF V,et al.Verification of a timed multitask system with UPPAAL[J].IEEE Transactions on Automation Science and Engineering,2010,7(4):921-932.
[30] DA SILVA O E A,DA SILVA L D,GORGONIO K,et al.Obtaining formal models from ladder diagrams[C]//Proceedings 9th IEEE International Conference on Industrial Informatics.Arapiraca:[s.n.],2011:796-801.
[31] TSAI J I,TENG C C.Constructing an abstract model for ladder diagram diagnosis using Petri nets[J].Asian Journal of Control,2010,12(3):309-322.
[32] 陈钢,宋晓宇,顾明.COQ定理证明器辅助PLC程序验证和分析[J].北京大学学报:自然科学版,2010,46(1):30-34.
[33] KRAMER B J,VAOLKER N.A highly dependable computing architecture for safety-critical control application[J].Real-Time Systems,1997,13(3):237-251.
[34] HUTH M,RYAN M.Logic in computer science[M].Cambridge:Cambridge Univercity Press,2004:172-254.
[35] 古天龙,徐周波.有序二叉决策图及应用[M].北京:科学出版社,2009:18-19.
[36] PAVLOVIC O,EHRICH H D.Model checking PLC software written in function block diagram[C]//Proceedings of the 3rd International Conference on Software Testing, Verification and Validation.Braunschweig:[s.n.],2010:439-448.
[37] GOURCUFF V,DE SMET O,FAURE J M.Efficient representation for formal verification of PLC programs[C]//Proceedings of the 8th International Workshop on Discrete Event Systems.Michigan:[s.n.],2006:182-187.
[38] HOLZMANN G J.The SIPN Model Checker[EB/OL].[2012-06-15] .http://spinroot.com/spin/whatispin.html.
[39] LUO Ji-liang,NONAMI K.Approach for transforming linear constraints on Petri nets[J].IEEE Transactions on Automatic Control,2011,56(12):2751-2765.
[40] XING Ke-yi,HU Bao-sheng,CHEN Hao-xun.Deadlock avoidance policy for Petri-net modeling of flexible manufacturing systems with shared resources[J].IEEE Transactions on Automatic Control,1996,41(2):289-295.
[41] LI Zhi-wu,ZHOU Meng-chu.Control of elementary and dependent siphons of Petri nets and their application[J].IEEE Trans Systems, Man, Cybernetics, Part A: Syst Humans,2008,38(1):133-148.