{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,18]],"date-time":"2025-10-18T20:26:08Z","timestamp":1760819168694},"reference-count":33,"publisher":"Elsevier BV","issue":"1","license":[{"start":{"date-parts":[[2002,1,1]],"date-time":"2002-01-01T00:00:00Z","timestamp":1009843200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[2013,7,17]],"date-time":"2013-07-17T00:00:00Z","timestamp":1374019200000},"content-version":"vor","delay-in-days":4215,"URL":"https:\/\/www.elsevier.com\/open-access\/userlicense\/1.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Science of Computer Programming"],"published-print":{"date-parts":[[2002,1]]},"DOI":"10.1016\/s0167-6423(01)00028-4","type":"journal-article","created":{"date-parts":[[2002,7,25]],"date-time":"2002-07-25T10:03:45Z","timestamp":1027591425000},"page":"101-113","source":"Crossref","is-referenced-by-count":18,"title":["Automated verification of function block-based industrial control systems"],"prefix":"10.1016","volume":"42","author":[{"given":"Norbert","family":"V\u00f6lker","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Bernd J.","family":"Kr\u00e4mer","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"78","reference":[{"key":"10.1016\/S0167-6423(01)00028-4_BIB1","series-title":"Proc. 11th Annu. IEEE Symp. on Logic in Computer Science","first-page":"207","article-title":"Reactive modules","author":"Alur","year":"1996"},{"issue":"3","key":"10.1016\/S0167-6423(01)00028-4_BIB2","doi-asserted-by":"crossref","first-page":"181","DOI":"10.1109\/32.489079","article-title":"Automatic symbolic verification of embedded systems","volume":"22","author":"Alur","year":"1996","journal-title":"IEEE Trans. Software Eng."},{"key":"10.1016\/S0167-6423(01)00028-4_BIB3","series-title":"An Introduction to Mathematical Logic and Type Theory: To Truth through Proof","author":"Andrews","year":"1986"},{"key":"10.1016\/S0167-6423(01)00028-4_BIB4","unstructured":"R. Boulton, A. Gordon, M. Gordon, J. Harrison, J. Herbert, J.V. Tassel, Experience with embedding hardware description languages in HOL, in: V. Stavridou, T. Melham, R. Boute (Eds.), Theorem Provers in Circuit Design, Proc. IFIP TC10\/WG 10.2 Internat. Conf. Nijmegen, June 1992, North-Holland, Amsterdam, 1992."},{"key":"10.1016\/S0167-6423(01)00028-4_BIB5","doi-asserted-by":"crossref","unstructured":"P. Curzon, The formal verification of the fairisle ATM switching element, Technical Report 329, Computer Laboratory, University of Cambridge, 1994.","DOI":"10.1145\/197917.198171"},{"key":"10.1016\/S0167-6423(01)00028-4_BIB6","series-title":"Introduction to HOL","author":"Gordon","year":"1993"},{"issue":"4","key":"10.1016\/S0167-6423(01)00028-4_BIB7","doi-asserted-by":"crossref","first-page":"301","DOI":"10.1093\/comjnl\/38.4.301","article-title":"Exploiting a graphical programming paradigm to facilitate rigorous verification of embedded software","volume":"38","author":"Halang","year":"1995","journal-title":"Comput. J."},{"key":"10.1016\/S0167-6423(01)00028-4_BIB8","series-title":"Synchronous Programming of Reactive Systems","author":"Halbwachs","year":"1993"},{"issue":"2","key":"10.1016\/S0167-6423(01)00028-4_BIB9","doi-asserted-by":"crossref","first-page":"157","DOI":"10.1023\/A:1008678014487","article-title":"Verification of real-time systems using linear relation analysis","volume":"11","author":"Halbwachs","year":"1997","journal-title":"Formal Methods System Des."},{"key":"10.1016\/S0167-6423(01)00028-4_BIB10","unstructured":"J. Harrison, Theorem proving with the real numbers, Ph.D. Thesis, Computer Laboratory, University of Cambridge, 1996."},{"key":"10.1016\/S0167-6423(01)00028-4_BIB11","doi-asserted-by":"crossref","unstructured":"J. Harrison, Floating point verification in HOL Light: the exponential function, Technical Report 428, Computer Laboratory, University of Cambridge, 1997.","DOI":"10.1007\/BFb0000475"},{"issue":"3","key":"10.1016\/S0167-6423(01)00028-4_BIB12","article-title":"Approximately time-optimal control of a two-tank system","volume":"14","author":"Heckenthaler","year":"1994","journal-title":"IEEE Control Systems Mag"},{"key":"10.1016\/S0167-6423(01)00028-4_BIB13","unstructured":"IEC International Standard 61131-3, Programmable Controllers, part 3: Programming Languages, International Electrotechnical Commission, 1993."},{"issue":"3","key":"10.1016\/S0167-6423(01)00028-4_BIB14","doi-asserted-by":"crossref","first-page":"24","DOI":"10.1109\/37.291460","article-title":"Approximately time-optimal fuzzy control of a two-tank system","volume":"14","author":"Heckenthaler","year":"1994","journal-title":"IEEE Control Systems"},{"key":"10.1016\/S0167-6423(01)00028-4_BIB15","unstructured":"S. Kowalewski, M. Fritz, H. Graf, S. S. J. Preu\u00dfig, O. Stursberg, H. Treseler, A case study in tool-aided analysis of discretely controlled continuous systems: the two tanks problem, in: Proc. 5th Internat. Workshop on Hybrid Systems (HSV), Notre Dame, USA, September 1997."},{"key":"10.1016\/S0167-6423(01)00028-4_BIB16","doi-asserted-by":"crossref","first-page":"237","DOI":"10.1023\/A:1007959310351","article-title":"A highly dependable computer architecture for safety-critical control applications","volume":"13","author":"Kr\u00e4mer","year":"1997","journal-title":"Real-Time Systems J"},{"key":"10.1016\/S0167-6423(01)00028-4_BIB17","unstructured":"L. Lamport, L. Paulson, Should your specification language be typed? Technical Report 425, Computer Laboratory, University of Cambridge, May 1997."},{"issue":"7","key":"10.1016\/S0167-6423(01)00028-4_BIB18","doi-asserted-by":"crossref","first-page":"18","DOI":"10.1109\/MC.1993.274940","article-title":"An investigation of the Thereac-25 accidents","volume":"26","author":"Leveson","year":"1993","journal-title":"IEEE Comput."},{"key":"10.1016\/S0167-6423(01)00028-4_BIB19","series-title":"The Temporal Logic of Reactive and Concurrent Systems: Specification","author":"Manna","year":"1992"},{"key":"10.1016\/S0167-6423(01)00028-4_BIB20","series-title":"The Definition of Standard ML (revised)","author":"Milner","year":"1997"},{"key":"10.1016\/S0167-6423(01)00028-4_BIB21","unstructured":"S. Morton, Specifying VDI\/VDE 3696 function blocks, MS Thesis, Department of Computer Science, University of the Witwatersrand, Johannesburg, 1998."},{"key":"10.1016\/S0167-6423(01)00028-4_BIB22","doi-asserted-by":"crossref","unstructured":"T. Nipkow, Higher-order unification, polymorphism, and subsorts, in: Proc. 2nd Internat. Workshop Conditional and Typed Rewriting Systems, Lecture Notes in Computer Science, Vol. 516, Springer, Berlin, 1991.","DOI":"10.1007\/3-540-54317-1_112"},{"key":"10.1016\/S0167-6423(01)00028-4_BIB23","doi-asserted-by":"crossref","unstructured":"T. Nipkow, D. von Oheimb, Java\u2113ight is type-safe\u2014definitely, in: Proc. 25th ACM Symp. Principles of Programming Languages, ACM Press, New York, 1998.","DOI":"10.1145\/268946.268960"},{"key":"10.1016\/S0167-6423(01)00028-4_BIB24","unstructured":"OMG, CORBA\/IIOP 2.2 Specification, 1998, On-line available via http:\/\/www.omg.org."},{"key":"10.1016\/S0167-6423(01)00028-4_BIB25","unstructured":"D. Parnas, J. Madey, M. Iglewski, Formal documentation of well-structured programs, Technical Report CLR 259, Communications Research Laboratory, Faculty of Engineering, Mc Master University, Hamilton, September 1992."},{"key":"10.1016\/S0167-6423(01)00028-4_BIB26","volume":"Vol. 828","author":"Paulson","year":"1994"},{"key":"10.1016\/S0167-6423(01)00028-4_BIB27","volume":"Vol. 4","author":"Reisig","year":"1995"},{"issue":"5","key":"10.1016\/S0167-6423(01)00028-4_BIB28","first-page":"424","article-title":"Knowledge intensive software engineering tools","volume":"4","author":"Rich","year":"1992","journal-title":"IEEE Trans. Software Eng."},{"key":"10.1016\/S0167-6423(01)00028-4_BIB29","series-title":"A less elementary tutorial for the PVS specification and verification system, Technical Report SRI-CSL-95-10, Computer Science Laboratory","author":"Rushby","year":"1995"},{"key":"10.1016\/S0167-6423(01)00028-4_BIB30","doi-asserted-by":"crossref","unstructured":"H. Sa\u0131\u0308di, The invariant checker: automated deductive verification of reactive systems, in: O. Grumberg (Ed.), Computer-Aided Verification, CAV \u201997, Lecture Notes in Computer Science, Vol. 1254, Springer, Berlin, 1997.","DOI":"10.1007\/3-540-63166-6_42"},{"issue":"2","key":"10.1016\/S0167-6423(01)00028-4_BIB31","doi-asserted-by":"crossref","first-page":"111","DOI":"10.1093\/comjnl\/38.2.111","article-title":"Formal specification and verification techniques for RISC pipeline conflicts","volume":"38","author":"Tahar","year":"1995","journal-title":"Comput. J."},{"key":"10.1016\/S0167-6423(01)00028-4_BIB32","unstructured":"VDI\/VDE Richtlinie 3696, Herstellerneutrale Konfigurierung von Prozessleitsystemem; Allgemeines zur herstellerneutralen Konfigurierung 1995 (in German)."},{"key":"10.1016\/S0167-6423(01)00028-4_BIB33","unstructured":"N. V\u00f6lker, Ein Rahmen zur Verifikation von SPS-Funktionsbausteinen in HOL, Ph.D. Thesis, FernUniversit\u00e4t Hagen, Shaker Verlag, 1998 (in German)."}],"container-title":["Science of Computer Programming"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0167642301000284?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0167642301000284?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2020,1,8]],"date-time":"2020-01-08T01:23:19Z","timestamp":1578446599000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S0167642301000284"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002,1]]},"references-count":33,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2002,1]]}},"alternative-id":["S0167642301000284"],"URL":"https:\/\/doi.org\/10.1016\/s0167-6423(01)00028-4","relation":{},"ISSN":["0167-6423"],"issn-type":[{"value":"0167-6423","type":"print"}],"subject":[],"published":{"date-parts":[[2002,1]]}}}