{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,15]],"date-time":"2024-09-15T17:49:56Z","timestamp":1726422596315},"reference-count":34,"publisher":"Elsevier BV","license":[{"start":{"date-parts":[[1999,1,1]],"date-time":"1999-01-01T00:00:00Z","timestamp":915148800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[2013,7,29]],"date-time":"2013-07-29T00:00:00Z","timestamp":1375056000000},"content-version":"vor","delay-in-days":5323,"URL":"http:\/\/creativecommons.org\/licenses\/by-nc-nd\/3.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Electronic Notes in Theoretical Computer Science"],"published-print":{"date-parts":[[1999]]},"DOI":"10.1016\/s1571-0661(04)00135-5","type":"journal-article","created":{"date-parts":[[2004,2,5]],"date-time":"2004-02-05T10:34:35Z","timestamp":1075977275000},"page":"97-110","source":"Crossref","is-referenced-by-count":2,"special_numbering":"C","title":["Automated Verification of Function Block Based Industrial Control Systems"],"prefix":"10.1016","volume":"25","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":[{"issue":"2","key":"10.1016\/S1571-0661(04)00135-5_NEWBIB1","doi-asserted-by":"crossref","first-page":"183","DOI":"10.1016\/0304-3975(94)90010-8","article-title":"A theory of timed automata","volume":"126","author":"Alur","year":"1994","journal-title":"Theoretical Computer Science"},{"key":"10.1016\/S1571-0661(04)00135-5_NEWBIB2","doi-asserted-by":"crossref","unstructured":"R. Alur and T. Henzinger. Reactive modules. In Proceedings, 11th Annual IEEE Symposium on Logic in Computer Science, pages 207\u2013218. IEEE Computer Society Press, 27\u201330, 1996.","DOI":"10.1109\/LICS.1996.561320"},{"issue":"3","key":"10.1016\/S1571-0661(04)00135-5_NEWBIB3","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 Transactions on Software Engineering"},{"key":"10.1016\/S1571-0661(04)00135-5_NEWBIB4","series-title":"An Introduction to Mathematical Logic and Type Theory: To Truth through Proof.","author":"Andrews","year":"1986"},{"key":"10.1016\/S1571-0661(04)00135-5_NEWBIB5","doi-asserted-by":"crossref","unstructured":"A. Benveniste and G. Berry. The synchronous approach to reactive and real-time systems. Proceedings of the IEEE 79(9), 1268\u20131282, 1991","DOI":"10.1109\/5.97297"},{"key":"10.1016\/S1571-0661(04)00135-5_NEWBIB6","unstructured":"R. Boulton, A. Gordon, M. Gordon, J. Harrison, J. Herbert, and J. V. Tassel. Experience with embedding hardware description languages in HOL. In V. Stavridou, T. Melham, and R. Boute (Eds.) Theorem Provers in Circuit Design. Proceedings of the IFIP TC10\/WG 10.2 International Conference, Nijmegen, June 1992. North-Holland, 1992."},{"key":"10.1016\/S1571-0661(04)00135-5_NEWBIB7","unstructured":"I. E. Commission. On-line at http:\/\/www.iec.ch."},{"key":"10.1016\/S1571-0661(04)00135-5_NEWBIB8","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\/S1571-0661(04)00135-5_NEWBIB9","series-title":"Introduction to HOL","author":"Gordon","year":"1993"},{"key":"10.1016\/S1571-0661(04)00135-5_NEWBIB10","doi-asserted-by":"crossref","first-page":"53","DOI":"10.1049\/sej.1992.0006","article-title":"Achieving high integrity of process control software by graphical design and formal verification","author":"Halang","year":"1992","journal-title":"IEE Software Engineering Journal"},{"key":"10.1016\/S1571-0661(04)00135-5_NEWBIB11","series-title":"Synchronous Programming of Reactive Systems","author":"Halbwachs","year":"1993"},{"issue":"2","key":"10.1016\/S1571-0661(04)00135-5_NEWBIB12","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 in System Design"},{"key":"10.1016\/S1571-0661(04)00135-5_NEWBIB13","unstructured":"J. Harrison. Theorem Proving with the Real Numbers. PhD thesis, Computer Laboratory, University of Cambridge, 1996."},{"key":"10.1016\/S1571-0661(04)00135-5_NEWBIB14","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\/S1571-0661(04)00135-5_NEWBIB15","article-title":"Approximately time-optimal control of a two-tank system","volume":"14","author":"Heckenthaler","year":"1994","journal-title":"IEEE Control Systems Magazine"},{"key":"10.1016\/S1571-0661(04)00135-5_NEWBIB16","unstructured":"IEC International Standard 1131\u20133. Programmable Controllers. Part 3: Programming Languages, 1993"},{"key":"10.1016\/S1571-0661(04)00135-5_NEWBIB17","unstructured":"S. Kowalewski, M. Fritz, H. Graf, S. S. J. Preu\u00dfig, O. Stursberg, and H. Treseler. A case study in tool-aided analysis of discretely controlled continuous systems: the two tanks problem. In Presented at the 5th Int. Workshop on Hybrid Systems (HS V), Notre Dame, USA, September 1997."},{"key":"10.1016\/S1571-0661(04)00135-5_NEWBIB18","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 Journal"},{"key":"10.1016\/S1571-0661(04)00135-5_NEWBIB19","unstructured":"L. Lamport and L. Paulson. Should your specification language be typed? Technical Report 425, Computer Laboratory, University of Cambridge, May 1997."},{"key":"10.1016\/S1571-0661(04)00135-5_NEWBIB20","series-title":"Programming industrial control systems using IEC 1131\u20133","author":"Lewis","year":"1995"},{"key":"10.1016\/S1571-0661(04)00135-5_NEWBIB21","series-title":"The Temporal Logic of Reactive and Concurrent Systems: Specification","author":"Manna","year":"1992"},{"key":"10.1016\/S1571-0661(04)00135-5_NEWBIB22","series-title":"The Definition of Standard ML (Revised)","author":"Milner","year":"1997"},{"key":"10.1016\/S1571-0661(04)00135-5_NEWBIB23","unstructured":"S. Morton. Specifying VDI\/VDE 3696 Function Blocks. Master Thesis, University of Witwatersrand, Johannesburg 1998."},{"key":"10.1016\/S1571-0661(04)00135-5_NEWBIB24","doi-asserted-by":"crossref","unstructured":"T. Nipkow. Higher-order unification, polymorphism, and subsorts. In Proc. 2nd Int. Workshop Conditional and Typed Rewriting Systems. LNCS 516, 1991.","DOI":"10.1007\/3-540-54317-1_112"},{"key":"10.1016\/S1571-0661(04)00135-5_NEWBIB25","doi-asserted-by":"crossref","unstructured":"T. Nipkow and D. von Oheimb. Javalight is type-safe\u2014definitely. In Proc. 25th ACM Symp. Principles of Programming Languages. ACM Press, 1998.","DOI":"10.1145\/268946.268960"},{"key":"10.1016\/S1571-0661(04)00135-5_NEWBIB26","unstructured":"Object Management Group (OMG). CORBA\/\/IIOP 2.2 Specification. Online at http:\/\/www.omg.org, 1998."},{"key":"10.1016\/S1571-0661(04)00135-5_NEWBIB27","unstructured":"D. Parnas, J. Madey, and M. Iglewski. Formal Documentation of Well-Structured Programs. Technical Report CLR 259, Faculty of Engineering, McMaster University, Hamilton, Ontario 1992"},{"key":"10.1016\/S1571-0661(04)00135-5_NEWBIB28","series-title":"Isabelle: A Generic Theorem Prover","author":"Paulson","year":"1994"},{"issue":"5","key":"10.1016\/S1571-0661(04)00135-5_NEWBIB29","first-page":"424","article-title":"Knowledge Intensive Software Engineering Tools","volume":"4","author":"Rich","year":"1992","journal-title":"IEEE Transactions on Software Engineering"},{"key":"10.1016\/S1571-0661(04)00135-5_NEWBIB30","unstructured":"J. Rushby and D. Stringer-Calvert. A less elementary tutorial for the PVS specification and verification system. Technical Report SRI-CSL-95\u201310, Computer Science Laboratory, SRI International, Menlo Park, CA, 1995. Revised, July 1996. Available, with specification files, from http:\/\/www.csl.sri.com\/csl-95-10.html."},{"key":"10.1016\/S1571-0661(04)00135-5_NEWBIB31","doi-asserted-by":"crossref","unstructured":"H. Sa\u00efdi. The Invariant Checker: Automated deductive verification of reactive systems. In O. Grumberg, editor, Computer-Aided Verification, CAV'97, volume 1254 of Lecture Notes in Computer Science. Springer-Verlag, 1997.","DOI":"10.1007\/3-540-63166-6_42"},{"issue":"2","key":"10.1016\/S1571-0661(04)00135-5_NEWBIB32","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":"The Computer Journal"},{"key":"10.1016\/S1571-0661(04)00135-5_NEWBIB33","unstructured":"VDI\/VDE Richtlinie 3696 Herstellerneutrale Konfigurierung von Proze\u00dfleitsystemem; Allgemeines zur herstellerneutralen Konfigurierung, 1995."},{"key":"10.1016\/S1571-0661(04)00135-5_NEWBIB34","doi-asserted-by":"crossref","unstructured":"N. V\u00f6lker. Ein Rahmen zur Verifikation von SPS-Funktionsbausteinen in HOL. PhD thesis, FernUniversit\u00e4t Hagen, Shaker Verlag, 1998.","DOI":"10.1007\/978-3-322-97661-1_5"}],"container-title":["Electronic Notes in Theoretical Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S1571066104001355?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S1571066104001355?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2019,2,15]],"date-time":"2019-02-15T06:57:02Z","timestamp":1550213822000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S1571066104001355"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1999]]},"references-count":34,"alternative-id":["S1571066104001355"],"URL":"https:\/\/doi.org\/10.1016\/s1571-0661(04)00135-5","relation":{},"ISSN":["1571-0661"],"issn-type":[{"value":"1571-0661","type":"print"}],"subject":[],"published":{"date-parts":[[1999]]}}}