{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,2]],"date-time":"2026-06-02T10:07:17Z","timestamp":1780394837122,"version":"3.54.1"},"reference-count":21,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2017,5,30]],"date-time":"2017-05-30T00:00:00Z","timestamp":1496102400000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2018,1]]},"DOI":"10.1007\/s10817-017-9415-7","type":"journal-article","created":{"date-parts":[[2017,5,30]],"date-time":"2017-05-30T13:26:17Z","timestamp":1496150777000},"page":"63-84","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":11,"title":["Translation of IEC\u00a061131-3 Function Block Diagrams to PVS for Formal Verification with Real-Time Nuclear Application"],"prefix":"10.1007","volume":"60","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-0245-8803","authenticated-orcid":false,"given":"Josh","family":"Newell","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Linna","family":"Pang","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"David","family":"Tremaine","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Alan","family":"Wassyng","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Mark","family":"Lawford","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2017,5,30]]},"reference":[{"key":"9415_CR1","unstructured":"Blech, J.O., Biha, S.O.: On formal reasoning on the semantics of PLC using Coq. CoRR abs\/1301.3047 (2013)"},{"key":"9415_CR2","first-page":"508","volume-title":"Formal Verification of Safety PLC Based Control Software","author":"D Darvas","year":"2016","unstructured":"Darvas, D., Majzik, I., Blanco Vi\u00f1uela, E.: Formal Verification of Safety PLC Based Control Software, pp. 508\u2013522. Springer, Cham (2016)"},{"key":"9415_CR3","unstructured":"DO-178C: Software Considerations in Airborne Systems and Equipment Certification. Special Committee 205 of RTCA (2011)"},{"key":"9415_CR4","unstructured":"IEC: 61131-3 Ed. 3.0 en:2013: Programmable Controllers\u2014Part 3: Programming Languages. International Electrotechnical Commission (2013)"},{"key":"9415_CR5","unstructured":"IEEE 7-4.3.2: Standard for Digital Computers in Safety Systems of Nuclear Power Generating Stations (Revision of IEEE Std 7-4.3.2-2003). The Institute of Electrical and Electronics Engineers (IEEE) (2010)"},{"key":"9415_CR6","doi-asserted-by":"crossref","unstructured":"Jimenez-Fraustro, F., Rutten, E.: A synchronous model of IEC 61131 PLC languages in SIGNAL. In: Euromicro Conference On Real-Time Systems, pp. 135\u2013142 (2001)","DOI":"10.1109\/EMRTS.2001.934016"},{"issue":"11","key":"9415_CR7","doi-asserted-by":"crossref","first-page":"980","DOI":"10.1016\/j.scico.2009.12.009","volume":"75","author":"Y Jin","year":"2010","unstructured":"Jin, Y., Parnas, D.L.: Defining the meaning of tabular mathematical expressions. Sci. Comput. Program. 75(11), 980\u20131000 (2010)","journal-title":"Sci. Comput. Program."},{"key":"9415_CR8","unstructured":"Joannou, P., Harauz, J., Viola, M., Cirjanic, R., Chan, D., Whittall, R., Tremaine, D., Moum, G.: Standard for Software Engineering of Safety Critical Software Revised for Application Oriented Language. CANDU Computer Systems Engineering Centre of Excellence Standard CE-1001-STD Rev. 3 (2014)"},{"issue":"5","key":"9415_CR9","doi-asserted-by":"crossref","first-page":"927","DOI":"10.1007\/s10796-016-9671-9","volume":"18","author":"J Nellen","year":"2016","unstructured":"Nellen, J., Driessen, K., Neuh\u00e4u\u00dfer, M., \u00c1brah\u00e1m, E., Wolters, B.: Two CEGAR-based approaches for the safety verification of PLC-controlled plants. Inf. Syst. Front. 18(5), 927\u2013952 (2016)","journal-title":"Inf. Syst. Front."},{"key":"9415_CR10","doi-asserted-by":"crossref","unstructured":"N\u00e9meth, E., Bartha, T.: Formal verification of safety functions by reinterpretation of functional block based specifications. In: Formal Methods for Industrial Critical Systems. Springer, pp. 199\u2013214 (2009)","DOI":"10.1007\/978-3-642-03240-0_17"},{"key":"9415_CR11","unstructured":"Newell, J., Pang, L., Tremaine, D., Wassyng, A., Lawford, M.: Formal translation of IEC 61131-3 function block diagrams to PVS with nuclear application. In: NASA Formal Methods\u20148th International Symposium, NFM 2016, Minneapolis, MN, USA, June 7\u20139, 2016, Proceedings. pp. 206\u2013220 (2016)"},{"key":"9415_CR12","doi-asserted-by":"crossref","unstructured":"Owre, S., Rushby, J.M., Shankar, N.: PVS: a prototype verification system. In: International Conference on Automated Deduction. LNCS, vol. 607, pp. 748\u2013752 (1992)","DOI":"10.1007\/3-540-55602-8_217"},{"key":"9415_CR13","unstructured":"Pang, L.: An Engineering Methodology for the Formal Verification of Function Block Based Systems. Ph.D. thesis, McMaster University, Department of Computing and Software (2015)"},{"key":"9415_CR14","doi-asserted-by":"crossref","first-page":"149","DOI":"10.1016\/j.scico.2015.10.005","volume":"113","author":"L Pang","year":"2015","unstructured":"Pang, L., Wang, C., Lawford, M., Wassyng, A.: Formal verification of function blocks applied to IEC 61131-3. Sci. Comput. Program. 113, 149\u2013190 (2015)","journal-title":"Sci. Comput. Program."},{"key":"9415_CR15","doi-asserted-by":"crossref","unstructured":"Pang, L., Wang, C., Lawford, M., Wassyng, A., Newell, J., Chow, V., Tremaine, D.: Formal verification of real-time function blocks using PVS. In: Proceedings 4th International Workshop on Engineering Safety and Security Systems, ESSS 2015, Oslo, Norway, June 22, 2015, pp. 65\u201379 (2015)","DOI":"10.4204\/EPTCS.184.5"},{"issue":"1","key":"9415_CR16","doi-asserted-by":"crossref","first-page":"41","DOI":"10.1016\/0167-6423(95)96871-J","volume":"25","author":"DL Parnas","year":"1995","unstructured":"Parnas, D.L., Madey, J.: Functional documents for computer systems. Sci. Comput. Program. 25(1), 41\u201361 (1995)","journal-title":"Sci. Comput. Program."},{"key":"9415_CR17","doi-asserted-by":"crossref","first-page":"948","DOI":"10.1109\/32.368133","volume":"20","author":"DL Parnas","year":"1994","unstructured":"Parnas, D.L., Madey, J., Iglewski, M.: Precise documentation of well-structured programs. IEEE Trans. Softw. Eng. 20, 948\u2013976 (1994)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"9415_CR18","doi-asserted-by":"crossref","first-page":"338","DOI":"10.1016\/j.arcontrol.2012.09.015","volume":"36","author":"D Soliman","year":"2012","unstructured":"Soliman, D., Thramboulidis, K., Frey, G.: Transformation of function block diagrams to Uppaal timed automata for the verification of safety applications. Annu. Rev. Control. 36, 338\u2013345 (2012)","journal-title":"Annu. Rev. Control."},{"issue":"1","key":"9415_CR19","doi-asserted-by":"crossref","first-page":"101","DOI":"10.1016\/S0167-6423(01)00028-4","volume":"42","author":"N V\u00f6lker","year":"2002","unstructured":"V\u00f6lker, N., Kr\u00e4mer, B.J.: Automated verification of function block-based industrial control systems. Sci. Comput. Program. 42(1), 101\u2013113 (2002)","journal-title":"Sci. Comput. Program."},{"key":"9415_CR20","unstructured":"Wassyng, A., Janicki, R.: Tabular expressions in software engineering. In: International Conference on Software & System Engineering and their Applications, vol. 4, pp. 1\u201346 (2003)"},{"key":"9415_CR21","doi-asserted-by":"crossref","unstructured":"Wassyng, A., Lawford, M.: Lessons learned from a successful implementation of formal methods in an industrial project. In: FME 2003: Formal Methods, LNCS, vol. 2805, pp. 133\u2013153. Springer, Berlin, Heidelberg (2003)","DOI":"10.1007\/978-3-540-45236-2_9"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10817-017-9415-7\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-017-9415-7.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-017-9415-7.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T21:18:54Z","timestamp":1750281534000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10817-017-9415-7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,5,30]]},"references-count":21,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2018,1]]}},"alternative-id":["9415"],"URL":"https:\/\/doi.org\/10.1007\/s10817-017-9415-7","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[2017,5,30]]}}}