{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,25]],"date-time":"2026-02-25T13:02:09Z","timestamp":1772024529101,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":24,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540231356","type":"print"},{"value":"9783540278634","type":"electronic"}],"license":[{"start":{"date-parts":[[2004,1,1]],"date-time":"2004-01-01T00:00:00Z","timestamp":1072915200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2004]]},"DOI":"10.1007\/978-3-540-27863-4_28","type":"book-chapter","created":{"date-parts":[[2010,9,16]],"date-time":"2010-09-16T16:51:50Z","timestamp":1284655910000},"page":"517-540","source":"Crossref","is-referenced-by-count":63,"title":["Verification of PLC Programs Given as Sequential Function Charts"],"prefix":"10.1007","author":[{"given":"Nanette","family":"Bauer","sequence":"first","affiliation":[]},{"given":"Sebastian","family":"Engell","sequence":"additional","affiliation":[]},{"given":"Ralf","family":"Huuck","sequence":"additional","affiliation":[]},{"given":"Sven","family":"Lohmann","sequence":"additional","affiliation":[]},{"given":"Ben","family":"Lukoschus","sequence":"additional","affiliation":[]},{"given":"Manuel","family":"Remelhe","sequence":"additional","affiliation":[]},{"given":"Olaf","family":"Stursberg","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"28_CR1","doi-asserted-by":"crossref","unstructured":"Lewis, R.: Programming industrial control systems using IEC 61131-3. IEE (1998)","DOI":"10.1049\/PBCE050E"},{"key":"28_CR2","unstructured":"International Electrotechnical Commission, Technical Committee No. 65: Programmable Controllers \u2013 Programming Languages, IEC 61131-3. (2003) Ed. 2.0"},{"key":"28_CR3","doi-asserted-by":"publisher","first-page":"67","DOI":"10.1002\/aic.690380107","volume":"38","author":"I. Moon","year":"1992","unstructured":"Moon, I., Powers, G.J., Burch, J.R., Clarke, E.M.: Automatic verification of sequential control systems using temporal logic. AIChE Journal\u00a038, 67\u201375 (1992)","journal-title":"AIChE Journal"},{"key":"28_CR4","doi-asserted-by":"publisher","first-page":"505","DOI":"10.1016\/S0005-1098(98)00179-4","volume":"35","author":"S. Kowalewski","year":"1999","unstructured":"Kowalewski, S., Engell, S., Preussig, J., Stursberg, O.: Verification of logic controllers for continuous plants using timed condition\/event system models. Automatica\u00a035, 505\u2013518 (1999)","journal-title":"Automatica"},{"key":"28_CR5","doi-asserted-by":"crossref","first-page":"247","DOI":"10.1007\/978-1-4615-4493-7_25","volume-title":"Discrete Event Systems","author":"S. Lamp\u00e9ri\u00e8re","year":"2000","unstructured":"Lamp\u00e9ri\u00e8re, S., Lesage, J.J.: Formal verification of the sequential part of PLC programs. In: Boel, R., Stremersch, G. (eds.) Discrete Event Systems, pp. 247\u2013254. Kluwer Academic Publishers, Dordrecht (2000)"},{"key":"28_CR6","unstructured":"Bauer, N., Huuck, R.: Towards automatic verification of embedded control software. In: Proc. 2nd Asia-Pacific Conf. on Quality Software, pp. 561\u2013567 (2001)"},{"key":"28_CR7","doi-asserted-by":"publisher","first-page":"626","DOI":"10.1145\/242223.242257","volume":"28","author":"E. Clarke","year":"1996","unstructured":"Clarke, E., Wing, J.: Formal methods: State of the art and future directions. ACM Computing Surveys\u00a028, 626\u2013643 (1996)","journal-title":"ACM Computing Surveys"},{"key":"28_CR8","volume-title":"Model Checking","author":"E. Clarke","year":"1999","unstructured":"Clarke, E., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (1999)"},{"key":"28_CR9","doi-asserted-by":"publisher","first-page":"303","DOI":"10.1016\/S0098-1354(00)00484-1","volume":"24","author":"K. Fujino","year":"2000","unstructured":"Fujino, K., Imafuku, K., Yamashita, Y., Nishitani, H.: Design and verification of the SFC program for sequential control. Comp. Chem. Eng.\u00a024, 303\u2013308 (2000)","journal-title":"Comp. Chem. Eng."},{"key":"28_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"149","DOI":"10.1007\/3-540-48057-9_13","volume-title":"Automata Implementation","author":"P. L\u2019Her","year":"1999","unstructured":"L\u2019Her, P., Scharbarg, J., Le Parc, P., Marce, L.: Proving sequential function chart programs using automata. In: Champarnaud, J.-M., Maurel, D., Ziadi, D. (eds.) WIA 1998. LNCS, vol.\u00a01660, pp. 149\u2013163. Springer, Heidelberg (1999)"},{"key":"28_CR11","doi-asserted-by":"crossref","unstructured":"Bornot, S., Huuck, R., Lakhnech, Y., Lukoschus, B.: Verification of sequential function charts using SMV. In: Proc. Int. Conf. on Parallel and Distributed Processing Techniques and Applications, pp. 2987\u20132993 (2000)","DOI":"10.1007\/978-1-4615-4493-7_26"},{"key":"28_CR12","unstructured":"McMillan, K.: The SMV Language. Cadence Berkeley Labs (1999), \n                    \n                      http:\/\/wwwcad.eecs.berkeley.edu\/kenmcmil\/language.ps"},{"key":"28_CR13","doi-asserted-by":"publisher","first-page":"142","DOI":"10.1016\/0890-5401(92)90017-A","volume":"98","author":"J.R. Burch","year":"1992","unstructured":"Burch, J.R., Clarke, E.M., McMillan, K.L., Dill, D.L., Hwang, L.: Symbolic model checking: 1020 states and beyond. Information and Comp.\u00a098, 142\u2013170 (1992)","journal-title":"Information and Comp."},{"key":"28_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"277","DOI":"10.1007\/3-540-48778-6_17","volume-title":"Formal Methods for Real-Time and Probabilistic Systems","author":"K. Havelund","year":"1999","unstructured":"Havelund, K., Larsen, K., Skou, A.: Formal verification of a power controller using the real-time model checker Uppaal2k. In: Katoen, J.-P. (ed.) AMAST-ARTS 1999, ARTS 1999, and AMAST-WS 1999. LNCS, vol.\u00a01601, pp. 277\u2013298. Springer, Heidelberg (1999)"},{"key":"28_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"400","DOI":"10.1007\/978-3-540-27863-4_22","volume-title":"Integration of Software Specification Techniques for Applications in Engineering","author":"N. Bauer","year":"2004","unstructured":"Bauer, N., Huuck, R., Lukoschus, B., Engell, S.: A unifying semantics for sequential function charts. In: Ehrig, H., Damm, W., Desel, J., Gro\u00dfe-Rhode, M., Reif, W., Schnieder, E., Westk\u00e4mper, E. (eds.) INT 2004. LNCS, vol.\u00a03147, pp. 400\u2013418. Springer, Heidelberg (2004)"},{"key":"28_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"52","DOI":"10.1007\/BFb0025774","volume-title":"Logics of Programs","author":"E. Clarke","year":"1982","unstructured":"Clarke, E., Emerson, E.: Synthesis of synchronisation skeletons for branching time temporal logic. In: Kozen, D. (ed.) Logic of Programs 1981. LNCS, vol.\u00a0131, pp. 52\u201371. Springer, Heidelberg (1982)"},{"key":"28_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"337","DOI":"10.1007\/3-540-11494-7_22","volume-title":"International Symposium on Programming","author":"J. Queille","year":"1982","unstructured":"Queille, J., Sifakis, J.: Specification and verification of concurrent systems in CESAR. In: Dezani-Ciancaglini, M., Montanari, U. (eds.) Programming 1982. LNCS, vol.\u00a0137, pp. 337\u2013350. Springer, Heidelberg (1982)"},{"key":"28_CR18","unstructured":"Bauer, N., Kowalewski, S., Sand, G., L\u00f6hl, T.: A case study: Multi product batch plant for the demonstration of control and scheduling problems. In: Proc. Analysis and Design of Mixed Processes, pp. 383\u2013388 (2000)"},{"key":"28_CR19","doi-asserted-by":"publisher","first-page":"76","DOI":"10.1109\/REAL.1995.495198","volume-title":"Proc. of the 16th IEEE Real-Time Systems Symposium","author":"K.G. Larsen","year":"1995","unstructured":"Larsen, K.G., Pettersson, P., Yi, W.: Compositional and Symbolic Model-Checking of Real-Time Systems. In: Proc. of the 16th IEEE Real-Time Systems Symposium, pp. 76\u201387. IEEE Computer Society Press, Los Alamitos (1995)"},{"key":"28_CR20","volume-title":"Proc. of 40th IEEE Conference on Decision and Control","author":"G. Behrmann","year":"2001","unstructured":"Behrmann, G., David, A., Larsen, K.G.: M ller, O., Pettersson, P., Yi, W.: Uppaal \u2013 present and future. In: Proc. of 40th IEEE Conference on Decision and Control, IEEE Computer Society Press, Los Alamitos (2001)"},{"key":"28_CR21","doi-asserted-by":"publisher","first-page":"134","DOI":"10.1007\/s100090050010","volume":"1","author":"K.G. Larsen","year":"1997","unstructured":"Larsen, K.G., Pettersson, P., Yi, W.: Uppaal in a Nutshell. Int. Journal on Software Tools for Technology Transfer\u00a01, 134\u2013152 (1997)","journal-title":"Int. Journal on Software Tools for Technology Transfer"},{"key":"28_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"263","DOI":"10.1007\/BFb0054177","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L. Aceto","year":"1998","unstructured":"Aceto, L., Bergueno, A., Larsen, K.G.: Model Checking via Reachability Testing for Timed Automata. In: Steffen, B. (ed.) TACAS 1998. LNCS, vol.\u00a01384, pp. 263\u2013280. Springer, Heidelberg (1998)"},{"key":"28_CR23","volume-title":"Handbook of graph grammars and computing by graph transformation: applications, languages, and tools","author":"H. Ehrig","year":"1999","unstructured":"Ehrig, H., Engels, G., Kreowski, H.J., Rozenberg, G.: Handbook of graph grammars and computing by graph transformation: applications, languages, and tools, vol.\u00a02. World Scientific Publishing Co., Inc., Singapore (1999)"},{"key":"28_CR24","unstructured":"Stursberg, O.: Analysis of switched continuous systems based on discretization. In: Proc. 4th Int. Conf. on Automation of Mixed Processes, pp. 73\u201378 (2000)"}],"container-title":["Lecture Notes in Computer Science","Integration of Software Specification Techniques for Applications in Engineering"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-27863-4_28","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,19]],"date-time":"2019-05-19T22:36:10Z","timestamp":1558305370000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-27863-4_28"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2004]]},"ISBN":["9783540231356","9783540278634"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-27863-4_28","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2004]]}}}