{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,12,10]],"date-time":"2025-12-10T12:18:27Z","timestamp":1765369107570,"version":"3.28.0"},"reference-count":40,"publisher":"IEEE","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2016,9]]},"DOI":"10.1109\/etfa.2016.7733717","type":"proceedings-article","created":{"date-parts":[[2016,11,7]],"date-time":"2016-11-07T21:26:20Z","timestamp":1478553980000},"page":"1-8","source":"Crossref","is-referenced-by-count":20,"title":["User-friendly formal specification languages - conclusions drawn from industrial experience on model checking"],"prefix":"10.1109","author":[{"given":"Antti","family":"Pakonen","sequence":"first","affiliation":[]},{"given":"Cheng","family":"Pang","sequence":"additional","affiliation":[]},{"given":"Igor","family":"Buzhinsky","sequence":"additional","affiliation":[]},{"given":"Valeriy","family":"Vyatkin","sequence":"additional","affiliation":[]}],"member":"263","reference":[{"key":"ref39","article-title":"Controlled natural language requirements in the design and analysis of safety critical I&C systems","author":"tommila","year":"2014","journal-title":"VTT-R-01067-14 VTT Espoo"},{"key":"ref38","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45657-0_29"},{"key":"ref33","first-page":"42","article-title":"A graphical property specification language","author":"lee","year":"1997","journal-title":"IEEE High-Assurance System Engineering Workshop"},{"key":"ref32","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE.2004.1317439"},{"key":"ref31","doi-asserted-by":"publisher","DOI":"10.1023\/A:1011227529550"},{"journal-title":"Symbolic Timing Diagrams a Visual Formalism for Model Verification","year":"2001","author":"shl\u00f6r","key":"ref30"},{"key":"ref37","article-title":"A Practical Introduction to PSL","author":"eisner","year":"2006","journal-title":"Springer Science"},{"year":"2012","key":"ref36"},{"article-title":"Visual Approaches for System Property Specification","year":"2003","author":"oh","key":"ref35"},{"journal-title":"Simulink Design Verifier Release Notes","year":"0","key":"ref34"},{"key":"ref10","doi-asserted-by":"publisher","DOI":"10.1109\/WODES.2006.1678428"},{"key":"ref40","article-title":"Practical model checking of LTL with Past","author":"pradella","year":"0","journal-title":"1 st International Workshop on Automated Technology for Verification and Analysis (ATVA03)"},{"key":"ref11","doi-asserted-by":"publisher","DOI":"10.1109\/ICST.2010.10"},{"key":"ref12","doi-asserted-by":"publisher","DOI":"10.1007\/s10664-012-9232-x"},{"key":"ref13","doi-asserted-by":"publisher","DOI":"10.1504\/IJITCC.2011.039285"},{"key":"ref14","doi-asserted-by":"publisher","DOI":"10.1109\/ETFA.2013.6648065"},{"key":"ref15","doi-asserted-by":"publisher","DOI":"10.1016\/j.ress.2012.03.021"},{"key":"ref16","doi-asserted-by":"publisher","DOI":"10.1109\/INDIN.2010.5549591"},{"key":"ref17","doi-asserted-by":"publisher","DOI":"10.5516\/NET.2009.41.1.079"},{"key":"ref18","article-title":"Analysis of an emergency diesel generator control system by compositional model checking - MODSAFE 2010 Work Report","author":"lahtinen","year":"2010","journal-title":"VTT Working Papers 156 VTT"},{"key":"ref19","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.1977.229904"},{"key":"ref28","first-page":"14","article-title":"Events and constraints: a graphical editor for capturing logic properties of programs","author":"smith","year":"2001","journal-title":"5th International Symposium on Requirements Engineering"},{"key":"ref4","doi-asserted-by":"publisher","DOI":"10.1145\/587051.587064"},{"key":"ref27","doi-asserted-by":"publisher","DOI":"10.1145\/192218.192226"},{"key":"ref3","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0053507"},{"key":"ref6","article-title":"Model Checking","author":"clarke","year":"1999","journal-title":"The MIT Press"},{"key":"ref29","article-title":"Timing Diagrams as Visual Specifications in Verification of Industrial Automation Controllers","volume":"2008","author":"vyatkin","year":"2007","journal-title":"Eurasip Journal of Embedded Systems"},{"key":"ref5","doi-asserted-by":"publisher","DOI":"10.1007\/s10515-007-0012-6"},{"key":"ref8","doi-asserted-by":"publisher","DOI":"10.1504\/IJMTM.2006.008802"},{"key":"ref7","doi-asserted-by":"publisher","DOI":"10.1109\/ISIE.2002.1026065"},{"key":"ref2","article-title":"Model Checking for Licensing Support in the Finnish Nuclear Industry","author":"pakonen","year":"2014","journal-title":"International Symposium on Future I&C for Nuclear Power Plants (ISOFTC 2004)"},{"key":"ref9","doi-asserted-by":"publisher","DOI":"10.3182\/20090610-3-IT-4004.00010"},{"journal-title":"BEL-V BfS CSN ISTec ONR SSM STUK","article-title":"Licensing of safety critical software for nuclear reactors — Common position of international nuclear regulators and authorised technical support organisations","year":"2014","key":"ref1"},{"key":"ref20","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-36577-X_3"},{"key":"ref22","doi-asserted-by":"publisher","DOI":"10.1145\/298595.298598"},{"key":"ref21","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2009.02.044"},{"key":"ref24","article-title":"Patter-based Analysis of Automated Production Systems","author":"campos","year":"2009","journal-title":"13th IFAC Symposium on Information Control Problems in Manufacturing"},{"key":"ref23","doi-asserted-by":"publisher","DOI":"10.1145\/302405.302672"},{"key":"ref26","doi-asserted-by":"publisher","DOI":"10.1093\/bioinformatics\/btn275"},{"key":"ref25","first-page":"5107","article-title":"Property Patterns for the Formal Verification of Automated Porductions Systems","author":"campos","year":"2008","journal-title":"137th IFAC World Congress"}],"event":{"name":"2016 IEEE 21st International Conference on Emerging Technologies and Factory Automation (ETFA)","start":{"date-parts":[[2016,9,6]]},"location":"Berlin, Germany","end":{"date-parts":[[2016,9,9]]}},"container-title":["2016 IEEE 21st International Conference on Emerging Technologies and Factory Automation (ETFA)"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx7\/7593665\/7733490\/07733717.pdf?arnumber=7733717","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2016,11,30]],"date-time":"2016-11-30T12:13:49Z","timestamp":1480508029000},"score":1,"resource":{"primary":{"URL":"http:\/\/ieeexplore.ieee.org\/document\/7733717\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016,9]]},"references-count":40,"URL":"https:\/\/doi.org\/10.1109\/etfa.2016.7733717","relation":{},"subject":[],"published":{"date-parts":[[2016,9]]}}}