{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,16]],"date-time":"2026-03-16T10:07:57Z","timestamp":1773655677659,"version":"3.50.1"},"reference-count":29,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2012,10,14]],"date-time":"2012-10-14T00:00:00Z","timestamp":1350172800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Empir Software Eng"],"published-print":{"date-parts":[[2014,6]]},"DOI":"10.1007\/s10664-012-9232-x","type":"journal-article","created":{"date-parts":[[2012,10,17]],"date-time":"2012-10-17T22:11:29Z","timestamp":1350511889000},"page":"655-677","source":"Crossref","is-referenced-by-count":9,"title":["An empirical study of control logic specifications for programmable logic controllers"],"prefix":"10.1007","volume":"19","author":[{"given":"Oscar","family":"Ljungkrantz","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Knut","family":"\u00c5kesson","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Martin","family":"Fabian","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Amir Hossein","family":"Ebrahimi","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2012,10,14]]},"reference":[{"key":"9232_CR1","doi-asserted-by":"crossref","unstructured":"Alur R, Henzinger TA (1992) Logics and models of real time: a survey. In: de Bakker J, Huizing K, de Roever WP, Rozenberg G (eds) Real time: theory in practice. Lecture notes in computer science, vol\u00a0600. Springer, pp\u00a074\u2013106","DOI":"10.1007\/BFb0031988"},{"key":"9232_CR2","unstructured":"Baier C, Katoen JP (2008) Principles of model checking. MIT Press"},{"key":"9232_CR3","doi-asserted-by":"crossref","unstructured":"Behrmann G, David A, Larsen KG (2004) A tutorial on Uppaal. In: Proceedings of the 4th international school on formal methods for the design of computer, communication, and software systems, Bertinoro, Italy. Lecture notes in computer science, vol\u00a03185, pp\u00a0200\u2013236","DOI":"10.1007\/978-3-540-30080-9_7"},{"key":"9232_CR4","doi-asserted-by":"crossref","unstructured":"B\u00e9rard B, Bidoit M, Finkel A, Laroussinie F, Petit A, Petrucci L, Schnoebelen P, McKenzie P (2001) Systems and software verification\u2014model-checking techniques and tools. Springer","DOI":"10.1007\/978-3-662-04558-9"},{"key":"9232_CR5","doi-asserted-by":"crossref","unstructured":"Bitsch F (2001) Safety patterns\u2014the key to formal specification of safety requirements. In: Proceedings of the 20th international conference on computer safety, reliability and security. Lecture notes in computer science, vol\u00a02187. Springer, pp\u00a0176\u2013189","DOI":"10.1007\/3-540-45416-0_18"},{"key":"9232_CR6","unstructured":"Bryman A, Bell E (2011) Business research methods, 3rd edn. Oxford University Press"},{"key":"9232_CR7","unstructured":"Campos JC, Machado J (2009) Pattern-based analysis of automated production systems. In: Proceedings of the 13th IFAC symposium on information control problems in manufacturing, Moscow, Russia, pp\u00a0976\u2013981"},{"key":"9232_CR8","unstructured":"Campos JC, Machado J, Seabra E (2008) Property patterns for the formal verification of automated production systems. In: Proceedings of the 17th IFAC world congress, IFAC, Seoul, South\u00a0Korea, pp\u00a05107\u20135112"},{"key":"9232_CR9","unstructured":"Clarke EM, Grumberg O, Peled DA (2000) Model checking. MIT Press"},{"key":"9232_CR10","unstructured":"Devlin K (2005) Sets, functions and logic\u2014an introduction to abstract mathematics, 3rd\u00a0edn. Chapman & Hall\/CRC"},{"key":"9232_CR11","doi-asserted-by":"crossref","unstructured":"Dwyer M, Avrunin G, Corbett J (1998) Property specification patterns for finite-state verification. In: Proceedings of the second workshop on formal methods in software practice, Clearwater Beach, Fla, USA, pp\u00a07\u201315","DOI":"10.1145\/298595.298598"},{"key":"9232_CR12","doi-asserted-by":"crossref","unstructured":"Dwyer M, Avrunin G, Corbett J (1999) Patterns in property specifications for finite-state verification. In: Proceedings of the 1999 international conference on software engineering, Los Angeles, CA, USA, pp\u00a0411\u2013420","DOI":"10.1145\/302405.302672"},{"key":"9232_CR13","doi-asserted-by":"crossref","unstructured":"Hajarnavis V, Young K (2008) An investigation into programmable logic controller software design techniques in the automotive industry. Assembly Autom 28:43\u201354","DOI":"10.1108\/01445150810849000"},{"key":"9232_CR14","unstructured":"IEC (2003) Programmable controllers\u2014part 3: programming languages, 2nd edn. International standard IEC 61131-3, International Electrotechnical Commission"},{"issue":"4","key":"9232_CR15","doi-asserted-by":"crossref","first-page":"791","DOI":"10.1109\/TASE.2010.2051664","volume":"7","author":"B Lennartson","year":"2010","unstructured":"Lennartson B, Bengtsson K, Yuan C, Andersson K, Fabian M, Falkman P, \u00c5kesson K (2010) Sequence planning for integrated product, process and automation design. IEEE Trans Autom Sci Eng 7(4):791\u2013802","journal-title":"IEEE Trans Autom Sci Eng"},{"key":"9232_CR16","doi-asserted-by":"crossref","unstructured":"Lewis RW (1998) Programming industrial control systems using IEC 1131-3 revised edition. The Institution of Electrical Engineers","DOI":"10.1049\/PBCE050E"},{"key":"9232_CR17","doi-asserted-by":"crossref","unstructured":"Ljungkrantz O, \u00c5kesson K, Fabian M (2010a) Practice of industrial control logic programming using library components. In: Guedes LA (ed) Programmable logic controller, Intech, chap\u00a02, pp\u00a017\u201332","DOI":"10.5772\/7191"},{"key":"9232_CR18","doi-asserted-by":"crossref","unstructured":"Ljungkrantz O, \u00c5kesson K, Fabian M, Yuan C (2010b) A formal specification language for PLC-based control logic. In: Proceedings of the 8th IEEE international conference on industrial informatics, Osaka, Japan, pp\u00a01067\u20131072","DOI":"10.1109\/INDIN.2010.5549591"},{"issue":"5","key":"9232_CR19","doi-asserted-by":"crossref","first-page":"725","DOI":"10.1016\/S1071-5819(03)00115-0","volume":"59","author":"M Lucas","year":"2003","unstructured":"Lucas M, Tilbury D (2003) A study of current logic design practices in the automotive manufacturing industry. Int J Human-Comput Stud 59(5):725\u2013753","journal-title":"Int J Human-Comput Stud"},{"key":"9232_CR20","doi-asserted-by":"crossref","unstructured":"Nain S, Vardi MY (2007) Branching vs. linear time: semantical perspective. In: Automated technology for verification and analysis. Lecture notes in computer science, vol 4762. Springer, pp\u00a019\u201334","DOI":"10.1007\/978-3-540-75596-8_4"},{"key":"9232_CR21","doi-asserted-by":"crossref","unstructured":"Preusse S, Hanisch HM (2008) Specification and verification of technical plant behavior with symbolic timing diagrams. In: Proceedings of the 3rd international design and test workshop, Monastir, Tunisia, pp\u00a0313\u2013318","DOI":"10.1109\/IDT.2008.4802520"},{"key":"9232_CR22","doi-asserted-by":"crossref","unstructured":"Preusse S, Hanisch HM (2009) Specification of technical plant behavior with a safety-oriented technical language. In: Proceedings of the 7th IEEE international conference on industrial informatics, Cardiff, Wales, pp\u00a0632\u2013637","DOI":"10.1109\/INDIN.2009.5195876"},{"issue":"3","key":"9232_CR23","doi-asserted-by":"crossref","first-page":"191","DOI":"10.1007\/s10696-006-9004-2","volume":"18","author":"J Richardsson","year":"2006","unstructured":"Richardsson J, Fabian M (2006) Modeling the control of a flexible manufacturing cell for automatic verification and control program generation. Flex Serv Manuf J 18(3):191\u2013208","journal-title":"Flex Serv Manuf J"},{"issue":"2","key":"9232_CR24","doi-asserted-by":"crossref","first-page":"163","DOI":"10.1016\/j.cosrev.2010.06.002","volume":"5","author":"KY Rozier","year":"2010","unstructured":"Rozier KY (2010) Linear temporal logic symbolic model checking. Comput Sci Rev 5(2):163\u2013203","journal-title":"Comput Sci Rev"},{"issue":"1","key":"9232_CR25","doi-asserted-by":"crossref","first-page":"67","DOI":"10.1023\/A:1024437214071","volume":"23","author":"J Ruf","year":"2003","unstructured":"Ruf J, Kropf T (2003) Symbolic verification and analysis of discrete timed systems. Formal Methods Syst Des 23(1):67\u2013108","journal-title":"Formal Methods Syst Des"},{"key":"9232_CR26","doi-asserted-by":"crossref","unstructured":"Shull F, Singer J, Sj\u00f8berg DIK (eds) (2008) Guide to advanced empirical software engineering, vol\u00a04334. Springer","DOI":"10.1007\/978-1-84800-044-5"},{"key":"9232_CR27","doi-asserted-by":"crossref","unstructured":"Vardi MY (2001) Branching vs. linear time: final showdown. In: Tools and algorithms for the construction and analysis of systems. Lecture notes in computer science, vol 2031. Springer, pp\u00a01\u201322","DOI":"10.1007\/3-540-45319-9_1"},{"key":"9232_CR28","first-page":"217","volume-title":"Proceedings of the empirical studies of programmers: second workshop","author":"W Visser","year":"1987","unstructured":"Visser W (1987) Strategies in programming programmable controllers: a field study on a professional programmer. In: Proceedings of the empirical studies of programmers: second workshop. Ablex Publishing Corp., Washington DC, pp\u00a0217\u2013230"},{"issue":"5","key":"9232_CR29","first-page":"5:1","volume":"2008","author":"V Vyatkin","year":"2008","unstructured":"Vyatkin V, Bouzon G (2008) Using visual specifications in verification of industrial automation controllers. EURASIP J Embedded Syst 2008(5):5:1\u20135:9","journal-title":"EURASIP J Embedded Syst"}],"container-title":["Empirical Software Engineering"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10664-012-9232-x.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10664-012-9232-x\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10664-012-9232-x","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,7,4]],"date-time":"2019-07-04T19:52:01Z","timestamp":1562269921000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10664-012-9232-x"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012,10,14]]},"references-count":29,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2014,6]]}},"alternative-id":["9232"],"URL":"https:\/\/doi.org\/10.1007\/s10664-012-9232-x","relation":{},"ISSN":["1382-3256","1573-7616"],"issn-type":[{"value":"1382-3256","type":"print"},{"value":"1573-7616","type":"electronic"}],"subject":[],"published":{"date-parts":[[2012,10,14]]}}}