{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,1,20]],"date-time":"2025-01-20T08:10:28Z","timestamp":1737360628187,"version":"3.33.0"},"publisher-location":"Berlin, Heidelberg","reference-count":49,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540666240"},{"type":"electronic","value":"9783540480921"}],"license":[{"start":{"date-parts":[[1999,1,1]],"date-time":"1999-01-01T00:00:00Z","timestamp":915148800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1999]]},"DOI":"10.1007\/3-540-48092-7_12","type":"book-chapter","created":{"date-parts":[[2007,8,10]],"date-time":"2007-08-10T17:01:46Z","timestamp":1186765306000},"page":"256-287","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Compilation and Synthesis for Real-Time Embedded Controllers"],"prefix":"10.1007","author":[{"given":"Martin","family":"Fr\u00e4nzle1","sequence":"first","affiliation":[]},{"given":"Markus","family":"M\u00fcller-Olm","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2000,3,24]]},"reference":[{"key":"12_CR1","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1016\/0304-3975(94)90010-8","volume":"126","author":"R. Alur","year":"1994","unstructured":"R. Alur and D. L. Dill. A theory of timed automata. Theoretical Computer Science, 126:183\u2013235, 1994.","journal-title":"Theoretical Computer Science"},{"key":"12_CR2","unstructured":"E. Asarin, P. Caspi, and O. Maler. A Kleene theorem for timed automata. In G. Winskel, editor, 12th Annual IEEE Symposium on Logic in Computer Science (LICS\u201897). IEEE Computer Society Press, 1997."},{"key":"12_CR3","series-title":"Lect Notes Comput Sci","volume-title":"Hybrid Systems II","author":"E. Asarin","year":"1995","unstructured":"E. Asarin, O. Maler, and A. Pnueli. Symbolic controller synthesis for discrete and timed systems. In P. Antsaklis, W. Kohn, A. Nerode, and S. Sastry, editors, Hybrid Systems II, LNCS 999, Springer-Verlag, 1995."},{"key":"12_CR4","series-title":"Lect Notes Comput Sci","first-page":"42","volume-title":"Stepwise Re nement of Distributed Systems-Models, Formalisms, Correctness. REX Workshop","author":"R. J. R. Back","year":"1989","unstructured":"R. J. R. Back and J. von Wright.Refinement calculus, Part I: Sequential nondeterministic programs. In J.W. de Bakker, W.-P. de Roever, and G. Rozenberg, editors, Stepwise Re nement of Distributed Systems-Models, Formalisms, Correctness. REX Workshop, LNCS 430, pages 42\u201366, Springer-Verlag, 1989."},{"issue":"7","key":"12_CR5","doi-asserted-by":"publisher","first-page":"583","DOI":"10.1007\/BF00259469","volume":"27","author":"R. J. R. Back","year":"1990","unstructured":"R. J. R. Back and J. von Wright. Duality in specification languages: A lattice theoretic approach. Acta Informatica, 27(7):583\u2013625, 1990.","journal-title":"Acta Informatica"},{"key":"12_CR6","unstructured":"G. Berry. The foundations of Esterel. In G. Plotkin, C. Stirling, and M. Tofte, editors, Proof, Language, and Interaction: Essays in Honour of Robin Milner. MITPress, to appear."},{"key":"12_CR7","doi-asserted-by":"crossref","unstructured":"W. R. Bevier, W. A. Hunt, J S. Moore, and W. D. Young. Special issue on system verification. Journal of Automated Reasoning, 5(4), 1989.","DOI":"10.1007\/BF00243131"},{"key":"12_CR8","unstructured":"J. P. Bowen, C. A. R. Hoare, H. Langmaack, E.-R. Olderog, and A. P. Ravn. A ProCoS II project final report: ESPRIT Basic Research project 7071. Bulletin of the European Association for Theoretical Computer Science (EATCS), 59, 1996."},{"key":"12_CR9","doi-asserted-by":"crossref","unstructured":"J. P. Bowen, M. Fr\u00e4nzle, E.-R. Olderog, and A. P. Ravn. Developing correct systems. In Proc. 5th Euromicro Workshop on Real-Time Systems, Oulu, Finland, pages 176\u2013189. IEEE Computer Society Press, 1993.","DOI":"10.1109\/EMWRT.1993.639088"},{"key":"12_CR10","doi-asserted-by":"crossref","unstructured":"G. M. Brown. Towards truly delay-insensitive circuit realizations of process algebras. In G. Jones and M. Sheeran, editors, Designing Correct Circuits, Workshops in Computing, pages 120\u2013131. Springer-Verlag, 1991.","DOI":"10.1007\/978-1-4471-3544-9_7"},{"key":"12_CR11","doi-asserted-by":"crossref","unstructured":"H. Dierks. Synthesizing controllers from real-time specifications. In Tenth International Symposium on System Synthesis (ISSS\u2019 97), pages 126\u2013133. IEEE Computer Society Press, 1997.","DOI":"10.1109\/ISSS.1997.621685"},{"key":"12_CR12","unstructured":"E. W. Dijkstra.A Discipline of Programming. Prentice Hall, 1976."},{"key":"12_CR13","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"168","DOI":"10.1007\/3-540-61648-9_40","volume-title":"Formal Techniques in Real-Time and Fault-Tolerant Systems (FTRTFT\u2019 96)","author":"M. Fr\u00e4nzle","year":"1996","unstructured":"M. Fr\u00e4nzle. Synthesizing controllers from duration calculus. In B. Jonsson and J. Parrow, editors, Formal Techniques in Real-Time and Fault-Tolerant Systems (FTRTFT\u2019 96), LNCS 1135, pages 168\u2013187, Springer-Verlag, 1996."},{"key":"12_CR14","unstructured":"M. Fr\u00e4nzle. Controller Design from Temporal Logic:Undecidability need not matter. Dissertation, Technische Fakult\u00e4t der Christian-Albrechts-Universit\u00e4t Kiel, Germany, 1997. Available as Bericht Nr. 9710, Institut f\u00fcr Informatik und Prakt. Mathematik der Christian-Albrechts-Universit\u00e4t Kiel, Germany, and via WWW under URL http:\/\/ca.informatik.uni-oldenburg.de\/~fraenzle\/diss.html ."},{"key":"12_CR15","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"294","DOI":"10.1007\/3-540-57877-3_20","volume-title":"Compiler Construction \u201894, 5th International Conference Edinburgh U.K.","author":"M. Fr\u00e4nzle","year":"1994","unstructured":"M. Fr\u00e4nzle and M. M\u00fcller-Olm. Towards provably correct code generation for a hard real-time programming language. In P. A. Fritzson, editor, Compiler Construction \u201894, 5th International Conference Edinburgh U.K., LNCS 786, pages 294\u2013308, Springer-Verlag, 1994."},{"key":"12_CR16","doi-asserted-by":"crossref","unstructured":"P. H. B. Gardiner and C. C. Morgan. Data refinement of predicate transformers. Theoretical Computer Science, 87, 1991. Also in [32].","DOI":"10.1016\/0304-3975(91)90029-2"},{"key":"12_CR17","doi-asserted-by":"crossref","first-page":"5","DOI":"10.1007\/978-1-4615-2339-0_1","volume":"8","author":"J. D. Guttman","year":"1995","unstructured":"J. D. Guttman, J. D. Ramsdell, and M. Wand. VLISP: A verified implementation of Scheme. Lisp and Symbolic Computation, 8:5\u201332, 1995.","journal-title":"A verified implementation of Scheme"},{"key":"12_CR18","doi-asserted-by":"crossref","unstructured":"N. Halbwachs. Synchronous Programming of Reactive Systems. Kluwer, 1993.","DOI":"10.1007\/978-1-4757-2231-4"},{"key":"12_CR19","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"214","DOI":"10.1007\/BFb0021726","volume-title":"Correct Hardware Design and Veri cation Methods","author":"H. Jifeng","year":"1993","unstructured":"He Jifeng, I. Page, and J. P. Bowen. Towards a provably correct hardware implementation of Occam. In G. J. Milne and L. Pierre, editors, Correct Hardware Design and Veri cation Methods, LNCS 683, pages 214\u2013225. Springer-Verlag, 1993."},{"key":"12_CR20","unstructured":"C. A. R. Hoare. Refinement algebra proves correctness of compiling specifications. In C. C. Morgan and J. C. P. Woodcock, editors, 3rd Re nement Workshop, Workshops in Computer Science, pages 33\u201348. Springer-Verlag, 1991."},{"issue":"8","key":"12_CR21","doi-asserted-by":"publisher","first-page":"672","DOI":"10.1145\/27651.27653","volume":"30","author":"C. A. R. Hoare","year":"1987","unstructured":"C. A. R. Hoare, I. J. Hayes, He Jifeng, C. C. Morgan, A.W. Roscoe, J. W. Sanders, I. H. Sorenson, J. M. Spivey, and B. A. Sufrin. Laws of programming. Communications of the ACM, 30(8):672\u2013687, 1987.","journal-title":"Communications of the ACM"},{"key":"12_CR22","doi-asserted-by":"publisher","first-page":"701","DOI":"10.1007\/BF01191809","volume":"30","author":"C. A. R. Hoare","year":"1993","unstructured":"C. A. R. Hoare, He Jifeng, and A. Sampaio. Normal form approach to compiler design. Acta Informatica, 30:701\u2013739, 1993.","journal-title":"Acta Informatica"},{"key":"12_CR23","unstructured":"inmos limited. Transputer Instruction Set-A Compiler Writer\u2019s Guide. Prentice Hall International, first edition, 1988."},{"key":"12_CR24","doi-asserted-by":"crossref","unstructured":"J. J. Joyce. Totally verified systems: Linking verified software to verified hardware. In Leeser and Brown [25], pages 177\u2013201.","DOI":"10.1007\/0-387-97226-9_29"},{"key":"12_CR25","series-title":"Lect Notes Comput Sci","volume-title":"Hardware Speci cation, Verification and Synthesis: Mathematical Aspects","year":"1990","unstructured":"M. Leeser and G. Brown, editors. Hardware Speci cation, Verification and Synthesis: Mathematical Aspects, LNCS 408, Springer-Verlag, 1990."},{"key":"12_CR26","doi-asserted-by":"crossref","unstructured":"O. Maler, A. Pnueli, and J. Sifakis. On the synthesis of discrete controllers for timed systems. In Meyer and Puech [29], pages 229\u2013242.","DOI":"10.1007\/3-540-59042-0_76"},{"key":"12_CR27","doi-asserted-by":"crossref","unstructured":"A. J. Martin. The design of a delay-insensitive microprocessor: An example of circuit synthesis by program transformation. In Leeser and Brown [25], pages 244\u2013259.","DOI":"10.1007\/0-387-97226-9_32"},{"key":"12_CR28","doi-asserted-by":"crossref","unstructured":"J. McCarthy and J. Painter. Correctness of a compiler for arithmetic expressions. In J. Schwarz, editor, Proc. Symp. Applied Mathematics, pages 33\u201341. American Mathematical Society, 1967.","DOI":"10.1090\/psapm\/019\/0242403"},{"key":"12_CR29","series-title":"Lect Notes Comput Sci","volume-title":"Symposium on Theoretical Aspects of Computer Science (STACS 95)","year":"1995","unstructured":"E.W. Meyer and C. Puech, editors. Symposium on Theoretical Aspects of Computer Science (STACS 95), LNCS 900, Springer-Verlag, 1995."},{"key":"12_CR30","unstructured":"R. Milner, M. Tofte, and R. Harper. The Definition of Standard ML. The MIT Press, 1990."},{"key":"12_CR31","unstructured":"J S. Moore. Piton, A Mechanically Verified Assembly-Level Language. Kluwer Academic Publishers, 1996."},{"key":"12_CR32","doi-asserted-by":"crossref","unstructured":"C. Morgan and T. Vickers (Eds.). On the Refinement Calculus. Springer-Verlag, 1994.","DOI":"10.1007\/978-1-4471-3273-8"},{"key":"12_CR33","doi-asserted-by":"crossref","unstructured":"F. L. Morris. Advice on structuring compilers and proving them correct. In Proceedings ACM Symposium on Principles of Programming Languages (PoPL\u201893), pages 144\u2013152, 1973.","DOI":"10.1145\/512927.512941"},{"key":"12_CR34","doi-asserted-by":"publisher","first-page":"287","DOI":"10.1016\/0167-6423(87)90011-6","volume":"9","author":"J. M. Morris","year":"1987","unstructured":"J. M. Morris. A theoretical basis for stepwise refinement and the programming calculus. Science of Computer Programming, 9:287\u2013306, 1987.","journal-title":"Science of Computer Programming"},{"key":"12_CR35","doi-asserted-by":"crossref","first-page":"287","DOI":"10.1007\/BF00276019","volume":"26","author":"J. M. Morris","year":"1989","unstructured":"J. M. Morris. Laws of data refinement. Acta Informatica, 26:287\u2013308, 1989.","journal-title":"Acta Informatica"},{"key":"12_CR36","volume-title":"ProCoS Technical Report Kiel MMO 14\/1","author":"M. M\u00fcller-Olm","year":"1995","unstructured":"M. M\u00fcller-Olm. A short description of the prototype compiler. ProCoS Technical Report Kiel MMO 14\/1, Christian-Albrechts-Universit\u00e4t Kiel, Germany, August 1995."},{"key":"12_CR37","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","DOI":"10.1007\/BFb0027453","volume-title":"Modular Compiler Verification: A Process-Algebraic Approach Advocating Stepwise Abstraction","author":"M. M\u00fcller-Olm","year":"1997","unstructured":"M. M\u00fcller-Olm. Modular Compiler Verification: A Process-Algebraic Approach Advocating Stepwise Abstraction, LNCS 1283, Springer-Verlag, 1997."},{"key":"12_CR38","doi-asserted-by":"crossref","unstructured":"T. S. Norvell. Machine code programs are predicates too. In D. Till, editor, 6th Refinement Workshop, Workshops in Computing. Springer-Verlag and British Computer Society, 1994.","DOI":"10.1007\/978-1-4471-3240-0_10"},{"issue":"7","key":"12_CR39","doi-asserted-by":"publisher","first-page":"654","DOI":"10.1093\/comjnl\/36.7.654","volume":"36","author":"D. J. Pavey","year":"1993","unstructured":"D. J. Pavey and L. A. Winsborrow. Demonstrating equivalence of source code and PROM contents. The Computer Journal, 36(7):654\u2013667, 1993.","journal-title":"The Computer Journal"},{"key":"12_CR40","unstructured":"A. P. Ravn. Design of Embedded Real-Time Computing Systems. Doctoral dissertation, Department of Computer Science, Danish Technical University, Lyngby, DK, 1995. Available as technical report ID-TR: 1995-170."},{"issue":"1","key":"12_CR41","doi-asserted-by":"publisher","first-page":"41","DOI":"10.1109\/32.210306","volume":"19","author":"A. P. Ravn","year":"1993","unstructured":"A. P. Ravn, H. Rischel, and K. M. Hansen. Specifying and verifying requirements of real-time systems. IEEE Transactions on Software Engineering, 19(1):41\u201355, 1993.","journal-title":"IEEE Transactions on Software Engineering"},{"key":"12_CR42","unstructured":"A. P. Ravn and H. Rischel. Real-time constraints in the ProCoS layers. In E. R. Olderog and B. Steffen, editors, Correct System Design, this volume."},{"key":"12_CR43","doi-asserted-by":"publisher","first-page":"223","DOI":"10.1016\/0304-3975(81)90080-3","volume":"15","author":"J. W. Thatcher","year":"1981","unstructured":"J. W. Thatcher, E. G. Wagner, and J. B. Wright. More on advice on structuring compilers and proving them correct. Theoretical Computer Science, 15:223\u2013249, 1981.","journal-title":"Theoretical Computer Science"},{"key":"12_CR44","doi-asserted-by":"crossref","unstructured":"W. Thomas. On the synthesis of strategies in infinite games. In Meyer and Puech [29], pages 1\u201313.","DOI":"10.1007\/3-540-59042-0_57"},{"key":"12_CR45","unstructured":"T. Wilke. Automaten und Logiken zur Beschreibung zeitabh\u00e4ngiger Systeme. Dissertation, Technische Fakult\u00e4t der Christian-Albrechts-Universit\u00e4t Kiel, Germany, 1994."},{"key":"12_CR46","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"694","DOI":"10.1007\/3-540-58468-4_191","volume-title":"Formal Techniques in Real-Time and Fault-Tolerant Systems (FTRTFT\u2019 94)","author":"T. Wilke","year":"1994","unstructured":"T. Wilke. Specifying timed state sequences in powerful decidable logics and timed automata. In H. Langmaack, W.-P. de Roever, and J. Vytopil, editors, Formal Techniques in Real-Time and Fault-Tolerant Systems (FTRTFT\u2019 94), LNCS 863, pages 694\u2013715, Springer-Verlag, 1994."},{"key":"12_CR47","doi-asserted-by":"publisher","first-page":"230","DOI":"10.1017\/S0305004100028322","volume":"49","author":"M.W. Wilkes","year":"1953","unstructured":"M.W. Wilkes and J. B. Stringer. Micro-programming and the design of the control circuits in an electronic digital computer. Proc. Cambridge Phil. Soc., 49:230\u2013238, 1953. also Annals of Hist. Comp. 8, 2 (dy1986) 121-126.","journal-title":"Proc. Cambridge Phil. Soc"},{"key":"12_CR48","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"58","DOI":"10.1007\/3-540-56503-5_8","volume-title":"Symposium on Theoretical Aspects of Computer Science (STACS 93)","author":"Z. Chaochen","year":"1993","unstructured":"Zhou Chaochen, M. R. Hansen, and P. Sestoft. Decidability and undecidability results for duration calculus. In P. Enjalbert, A. Finkel, and K. W. Wagner, editors, Symposium on Theoretical Aspects of Computer Science (STACS 93), LNCS 665, pages 58\u201368, Springer-Verlag, 1993."},{"issue":"5","key":"12_CR49","doi-asserted-by":"publisher","first-page":"269","DOI":"10.1016\/0020-0190(91)90122-X","volume":"40","author":"Z. Chaochen","year":"1991","unstructured":"Zhou Chaochen, C. A. R. Hoare, and A. P. Ravn. A calculus of durations. Information Processing Letters, 40(5):269\u2013276, 1991.","journal-title":"Information Processing Letters"}],"container-title":["Lecture Notes in Computer Science","Correct System Design"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-48092-7_12","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,20]],"date-time":"2025-01-20T07:42:43Z","timestamp":1737358963000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-48092-7_12"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1999]]},"ISBN":["9783540666240","9783540480921"],"references-count":49,"URL":"https:\/\/doi.org\/10.1007\/3-540-48092-7_12","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[1999]]},"assertion":[{"value":"24 March 2000","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}