{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,12]],"date-time":"2026-03-12T14:01:07Z","timestamp":1773324067349,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":31,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540690955","type":"print"},{"value":"9783540691006","type":"electronic"}],"license":[{"start":{"date-parts":[[2008,1,1]],"date-time":"2008-01-01T00:00:00Z","timestamp":1199145600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2008,1,1]],"date-time":"2008-01-01T00:00:00Z","timestamp":1199145600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2008]]},"DOI":"10.1007\/978-3-540-69100-6_9","type":"book-chapter","created":{"date-parts":[[2008,6,5]],"date-time":"2008-06-05T09:27:49Z","timestamp":1212658069000},"page":"121-136","source":"Crossref","is-referenced-by-count":23,"title":["Ladder Metamodeling and PLC Program Validation through Time Petri Nets"],"prefix":"10.1007","author":[{"given":"Darlam Fabio","family":"Bender","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Beno\u00eet","family":"Combemale","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Xavier","family":"Cr\u00e9gut","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jean Marie","family":"Farines","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Bernard","family":"Berthomieu","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Fran\u00e7ois","family":"Vernadat","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"issue":"4","key":"9_CR1","doi-asserted-by":"publisher","first-page":"477","DOI":"10.1016\/S0952-1976(00)00014-2","volume":"13","author":"A. Guasch","year":"2000","unstructured":"Guasch, A., Quevedo, J., Milne, R.: Fault diagnosis for gas turbines based on the control system. Engineering Applications of Artificial Intelligence\u00a013(4), 477\u2013484 (2000)","journal-title":"Engineering Applications of Artificial Intelligence"},{"key":"9_CR2","unstructured":"International Electrotechnical Comission: IEC 61131-3 International Standard, Programmable Controllers, Part 3: Programming Languages (2003)"},{"key":"9_CR3","first-page":"210","volume-title":"SAFECOMP 1997: the 16th International Conference on Computer Safety, Reliability and Security York","author":"K. Tourlas","year":"1997","unstructured":"Tourlas, K.: An assessment of the IEC 1131 -3 standard on languages for programmable controllers. In: Daniel, P. (ed.) SAFECOMP 1997: the 16th International Conference on Computer Safety, Reliability and Security York, UK, September 7-10, 1997, pp. 210\u2013219. Springer, Heidelberg (1997)"},{"key":"9_CR4","volume-title":"Locksmithing and Electronic Security Wiring Diagrams","author":"J.L. Schum","year":"2002","unstructured":"Schum, J.L.: Locksmithing and Electronic Security Wiring Diagrams. McGraw-Hill Professional, New York (2002)"},{"key":"9_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"184","DOI":"10.1007\/BFb0054172","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A. Aiken","year":"1998","unstructured":"Aiken, A., F\u00e4hndrich, M., Su, Z.: Detecting races in relay ladder logic programs. In: Steffen, B. (ed.) ETAPS 1998 and TACAS 1998. LNCS, vol.\u00a01384, pp. 184\u2013200. Springer, Heidelberg (1998)"},{"issue":"9","key":"9_CR6","doi-asserted-by":"publisher","first-page":"1036","DOI":"10.1109\/TCOM.1976.1093424","volume":"24","author":"P. Merlin","year":"1976","unstructured":"Merlin, P., Farber, D.: Recoverability of communication protocols\u2013implications of a theoretical study. Communications, IEEE Transactions on [legacy, pre - 1988]\u00a024(9), 1036\u20131043 (1976)","journal-title":"Communications, IEEE Transactions on [legacy, pre - 1988]"},{"key":"9_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"128","DOI":"10.1007\/11663430_14","volume-title":"Satellite Events at the MoDELS 2005 Conference","author":"F. Jouault","year":"2006","unstructured":"Jouault, F., Kurtev, I.: Transforming Models with ATL. In: Bruel, J.-M. (ed.) MoDELS 2005. LNCS, vol.\u00a03844, pp. 128\u2013138. Springer, Heidelberg (2006)"},{"key":"9_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"128","DOI":"10.1007\/978-3-540-24756-2_8","volume-title":"Integrated Formal Methods","author":"S. Chaki","year":"2004","unstructured":"Chaki, S., Clarke, E.M., Ouaknine, J., Sharygina, N., Sinha, N.: State\/event-based software model checking. In: Boiten, E.A., Derrick, J., Smith, G.P. (eds.) IFM 2004. LNCS, vol.\u00a02999, pp. 128\u2013147. Springer, Heidelberg (2004)"},{"issue":"14","key":"9_CR9","doi-asserted-by":"publisher","first-page":"2741","DOI":"10.1080\/00207540412331312688","volume":"42","author":"B. Berthomieu","year":"2004","unstructured":"Berthomieu, B., Ribet, P.O., Vernadat, F.: The tool TINA \u2013 construction of abstract state spaces for Petri nets and time Petri nets. International Journal of Production Research\u00a042(14), 2741\u20132756 (2004)","journal-title":"International Journal of Production Research"},{"key":"9_CR10","unstructured":"Berthomieu, B., Vernadat, F.: Time petri nets analysis with tina. In: Third International Conference on Quantitative Evaluation of Systems, 2006. QEST 2006, pp. 123\u2013124 (2006)"},{"key":"9_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"516","DOI":"10.1007\/978-3-540-75596-8_37","volume-title":"Automated Technology for Verification and Analysis","author":"B. Berthomieu","year":"2007","unstructured":"Berthomieu, B., Peres, F., Vernadat, F.: Model-checking bounded prioritrized time petri nets. In: Namjoshi, K.S., Yoneda, T., Higashino, T., Okamura, Y. (eds.) ATVA 2007. LNCS, vol.\u00a04762, pp. 516\u2013535. Springer, Heidelberg (2007)"},{"issue":"1","key":"9_CR12","doi-asserted-by":"publisher","first-page":"7","DOI":"10.1023\/A:1011276507260","volume":"19","author":"E.M. Clarke","year":"2001","unstructured":"Clarke, E.M., Biere, A., Raimi, R., Zhu, Y.: Bounded model checking using satisfiability solving. Formal Methods in System Design\u00a019(1), 7\u201334 (2001)","journal-title":"Formal Methods in System Design"},{"key":"9_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"516","DOI":"10.1007\/3-540-61363-3_28","volume-title":"Application and Theory of Petri Nets 1996","author":"F. Vernadat","year":"1996","unstructured":"Vernadat, F., Az\u00e9ma, P., Michel, F.: Covering step graph. In: Billington, J., Reisig, W. (eds.) ICATPN 1996. LNCS, vol.\u00a01091, pp. 516\u2013535. Springer, Heidelberg (1996)"},{"key":"9_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-60761-7","volume-title":"Partial-Order Methods for the Verification of Concurrent Systems","author":"P. Godefroid","year":"1996","unstructured":"Godefroid, P.: Partial-Order Methods for the Verification of Concurrent Systems. LNCS, vol.\u00a01032. Springer, Heidelberg (1996)"},{"key":"9_CR15","unstructured":"Jimenez, I., Lopez, E., Ramirez, A.: Synthesis of ladder diagrams from petri nets controller models. In: Proceedings of the 2001 IEEE International Symposium on Intelligent Control, 2001 (ISIC 2001), pp. 225\u2013230 (2001)"},{"key":"9_CR16","doi-asserted-by":"crossref","unstructured":"Minas, M., Frey, G.: Visual plc-programming using signal interpreted petri nets. In: American Control Conference, 2002. Proceedings of the 2002, vol.\u00a06, pp. 5019\u20135024 (2002)","DOI":"10.1109\/ACC.2002.1025461"},{"key":"9_CR17","unstructured":"Klein, S., Frey, G., Litz, L.: A petri net based approach to the development of correct logic controllers. In: Proceedings of the 2nd International Workshop on Integration of Specification Techniques for Applications in Engineering (INT 2002), Grenoble (France), pp. 116\u2013129 (2002)"},{"key":"9_CR18","volume-title":"Design and formal Analysis of Petri Net based Logic Control Algorithms (Dissertation, University of Kaiserslautern).","author":"G. Frey","year":"2002","unstructured":"Frey, G.: Design and formal Analysis of Petri Net based Logic Control Algorithms (Dissertation, University of Kaiserslautern). Shaker Verlag, Aachen (2002)"},{"issue":"1","key":"9_CR19","doi-asserted-by":"publisher","first-page":"61","DOI":"10.1016\/S0304-3975(00)00089-X","volume":"253","author":"H. Dierks","year":"2001","unstructured":"Dierks, H.: PLC-automata: a new class of implementable real-time automata. Theoretical Computer Science\u00a0253(1), 61\u201393 (2001)","journal-title":"Theoretical Computer Science"},{"key":"9_CR20","unstructured":"Heiner, M., Menzel, T.: Instruction list verification using a petri net semantics (1998)"},{"key":"9_CR21","unstructured":"Heiner, M., Menzel, T.: A petri net semantics for the plc language instruction list. In: IEE workshop on discrete event systems (1998)"},{"key":"9_CR22","doi-asserted-by":"crossref","unstructured":"Canet, G., Couffin, S., Lesage, J.J., Petit, A., Schnoebelen, P.: Towards the automatic verification of plc programs written in instruction list. In: 2000 IEEE International Conference on Systems, Man, and Cybernetics, vol.\u00a04, pp. 2449\u20132454 (2000)","DOI":"10.1109\/ICSMC.2000.884359"},{"issue":"2","key":"9_CR23","doi-asserted-by":"publisher","first-page":"53","DOI":"10.1109\/37.272781","volume":"14","author":"I. Moon","year":"1994","unstructured":"Moon, I.: Modeling programmable logic controllers for logic verification. Control Systems Magazine, IEEE\u00a014(2), 53\u201359 (1994)","journal-title":"Control Systems Magazine, IEEE"},{"key":"9_CR24","unstructured":"Rausch, M., Krogh, B.: Transformations between different model forms in discrete event systems. In: Computational Cybernetics and Simulation, 1997 IEEE International Conference on Systems, Man, and Cybernetics, 1997, October 12-15, 1997, vol.\u00a03, pp. 2841\u20132846 (1997)"},{"key":"9_CR25","unstructured":"Bohumir Zoubek, J.M.R., Kwiatkowska, M.: Towards automatic verification of ladder logic programs. In: Proc. IMACS Multiconference on Computational Engineering in Systems Applications (CESA) (2003)"},{"key":"9_CR26","unstructured":"Huuck, R.: Software Verification for Programmable Logic Controllers. PhD thesis, Institute of Computer Science and Applied Mathematics, University of Kiel (2003)"},{"key":"9_CR27","doi-asserted-by":"crossref","unstructured":"Berthomieu, B., Farail, P., Gaufillet, P., Peres, F., Bodeveix, J.P., Filali, M., Saad, R., Vernadat, F., Garavel, H., Lang, F.: FIACRE: an intermediate language for model verification in the TOPCASED environment. In: European Congress on Embedded Real-Time Software (ERTS), Toulouse SEE (electronic medium) (2008), http:\/\/www.see.asso.fr","DOI":"10.1007\/978-3-642-01924-1_15"},{"key":"9_CR28","unstructured":"Vernadat, F., Percebois, C., Farail, P., Vingerhoeds, R., Rossignol, A., Talpin, J.P., Chemouil, D.: The TOPCASED Project - A Toolkit in OPen-source for Critical Applications and SystEm Development. In: Data Systems In Aerospace (DASIA), Berlin, Germany, 22\/05\/2006-25\/05\/2006, European Space Agency (ESA Publications) (2006), http:\/\/www.esa.int\/publications (electronic medium)"},{"key":"9_CR29","volume-title":"Enterprise Information System IX","author":"B. Combemale","year":"2008","unstructured":"Combemale, B., Cr\u00e9gut, X., Garoche, P.L., Thirioux, X., Vernadat, F.: A Property-Driven Approach to Formal Verification of Process Models. In: Cardoso, J., Cordeiro, J., Filipe, J., Pedrosa, V. (eds.) Enterprise Information System IX. Springer, Heidelberg (2008)"},{"key":"9_CR30","unstructured":"Nikora, A.P.: Developing formal correctness properties from natural language requirements. NASA: Jet Propulsion Laboratory (2006)"},{"key":"9_CR31","doi-asserted-by":"crossref","unstructured":"Jouault, F., B\u00e9zivin, J., Kurtev, I.: TCS: a DSL for the Specification of Textual Concrete Syntaxes in Model Engineering. In: 5th international conference on Generative Programming and Component Engineering (GPCE 2006) (October 2006)","DOI":"10.1145\/1173706.1173744"}],"container-title":["Lecture Notes in Computer Science","Model Driven Architecture \u2013 Foundations and Applications"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-69100-6_9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,30]],"date-time":"2025-01-30T15:49:53Z","timestamp":1738252193000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-540-69100-6_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2008]]},"ISBN":["9783540690955","9783540691006"],"references-count":31,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-69100-6_9","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2008]]}}}