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.
[2]
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.
FREY G,LITZ L.Formal methods in PLC programming[C]//International Conference on Systems, Man and Cybernetics, Tennessee.Nashville:IEEE Press,2000:2431-2436.
[6]
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.
[7]
PELED D A.Software reliability methods[M].New York:Springer-Verlag,2001:1-9.
[8]
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.
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.
[11]
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.
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.
[16]
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.
[17]
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.
[18]
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.
[19]
FREY G,LITZ L.Correctness analysis of Petri net based logic controllers[C]//Proceedings of American Control Conference.Chicago:[s.n.],2000:3165-3166.
[20]
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.
[21]
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.
[22]
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.
[23]
ALUR R,DILL D L.A theory of timed automata[J].Theoretical Computer Science,1994,26(2):183-235.
[24]
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.
[25]
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.
[26]
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.
[27]
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.
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.
[30]
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.
[31]
BEHRMANN G,DAVID A,LARSEN K G.A tutorial on uppaal[J].Lecture Notes in Computer Science,2004,3185:33-35.
[32]
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.
[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.
