{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,12,18]],"date-time":"2025-12-18T13:56:23Z","timestamp":1766066183273},"publisher-location":"Berlin, Heidelberg","reference-count":84,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540584681"},{"type":"electronic","value":"9783540489849"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1994]]},"DOI":"10.1007\/3-540-58468-4_171","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T16:14:53Z","timestamp":1330272893000},"page":"288-335","source":"Crossref","is-referenced-by-count":38,"title":["Provably Correct Systems"],"prefix":"10.1007","author":[{"given":"Jifeng","family":"He","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"C. A. R.","family":"Hoare","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Martin","family":"Fr\u00c4nzle","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Markus","family":"M\u00fcller-Olm","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ernst-R\u00fcdiger","family":"Olderog","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Michael","family":"Schenke","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Michael R.","family":"Hansen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Anders P.","family":"Ravn","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Hans","family":"Rischel","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,6,8]]},"reference":[{"key":"15_CR1","unstructured":"R. J. R. Back. Refinement calculus, part II: Parallel and reactive programs. In J. W. de Bakker, W.-P. de Roever, and G. Rozenberg, editors, Stepwise Refinement of Distributed Systems: Models, Formalisms, Correctness, volume 430 of LNCS, pages 67\u201393, 1990."},{"key":"15_CR2","unstructured":"J. C. M. Baeten and P. Weijland. Process Algebra. Cambridge University Press, 1980."},{"key":"15_CR3","doi-asserted-by":"crossref","unstructured":"F. L. Bauer et al. The Munich Project CIP, Volume II: The Transformation System CIP-S, volume 292 of LNCS. Springer-Verlag, 1987.","DOI":"10.1007\/3-540-18779-0"},{"key":"15_CR4","volume-title":"Technical Report 5","author":"W. R. Bevier","year":"1987","unstructured":"W. R. Bevier, W. A. Hunt, Jr., and W. D. Young. Towards verified execution environments. Technical Report 5, Computational Logic, Inc., Austin, Texas, USA, February 1987."},{"key":"15_CR5","volume-title":"ProCoS Technical Report [ID\/DTH DB 13\/1]","author":"D. Bj\u00d8rner","year":"1993","unstructured":"D. Bj\u00d8rner, H. Langmaack, and C. A. R. Hoare. ProCoS I final deliverable. ProCoS Technical Report [ID\/DTH DB 13\/1], Department of Computer Science, Technical University of Denmark, DK-2800 Lyngby, Denmark, January 1993."},{"key":"15_CR6","unstructured":"Egon B\u00f6rger, Igor Durdanovic, and Dean Rosenzweig. Occam: Specification and compiler correctness \u2014 Part I: The primary model. unpublished note."},{"key":"15_CR7","doi-asserted-by":"crossref","unstructured":"A. Bouajjani, R. Echahed, and R. Robbana. Verifying invariance properties of timed systems with duration variables. In these proceedings, 1994.","DOI":"10.1007\/3-540-58468-4_166"},{"key":"15_CR8","unstructured":"J. P. Bowen, editor. Towards Verified Systems. Real-Time Safety Critical Systems Series. Elsevier, in press."},{"key":"15_CR9","doi-asserted-by":"crossref","unstructured":"J. P. Bowen, M. Fr\u00c4nzle, E.-R. Olderog, and A. P. Ravn. Developing correct systems. In Proc. 5th Euromicro Workshop on Real-Time Systems, pages 176\u2013189. IEEE Computer Society Press, June 1993.","DOI":"10.1109\/EMWRT.1993.639088"},{"key":"15_CR10","doi-asserted-by":"crossref","unstructured":"J. P. Bowen, He Jifeng, and I. Page. Hardware compilation. In Bowen [8], chapter 10, pages 193\u2013207.","DOI":"10.1016\/B978-0-444-89901-9.50019-7"},{"issue":"4","key":"15_CR11","doi-asserted-by":"crossref","first-page":"189","DOI":"10.1049\/sej.1993.0025","volume":"8","author":"J. P. Bowen","year":"1993","unstructured":"J. P. Bowen and V. Stavridou. Safety-critical systems, formal methods and standards. IEE\/BCS Software Engineering Journal, 8(4):189\u2013209, July 1993.","journal-title":"IEE\/BCS Software Engineering Journal"},{"key":"15_CR12","volume-title":"ProCoS Technical Report [OU HJF 12\/2]","author":"S. Brien","year":"1993","unstructured":"S. Brien, M. Engel, He Jifeng, A. P. Ravn, and H. Rischel. Z model for Duration Calculus. ProCoS Technical Report [OU HJF 12\/2], Oxford University Computing Laboratory, UK, September 1993."},{"key":"15_CR13","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":"15_CR14","doi-asserted-by":"crossref","first-page":"236","DOI":"10.1016\/0022-0000(87)90026-2","volume":"34","author":"M. Broy","year":"1987","unstructured":"M. Broy. Specification and top-down design of distributed systems. J. Comput. System Sci., 34:236\u2013265, 1987.","journal-title":"J. Comput. System Sci."},{"key":"15_CR15","volume-title":"volume 16 of LNCS","author":"R. H. Campbell","year":"1974","unstructured":"R. H. Campbell and A. N. Habermann. The specification of process synchronisation by path expressions. In E. Gelenbe and C. Kaiser, editors, Operating Systems, International Symposium, Rocquencourt 1974, volume 16 of LNCS. Springer-Verlag, 1974."},{"key":"15_CR16","doi-asserted-by":"crossref","unstructured":"K. M. Chandy and J. Misra. Parallel Program Design: A Foundation. Addison-Wesley, 1988.","DOI":"10.1007\/978-1-4613-9668-0_6"},{"key":"15_CR17","doi-asserted-by":"crossref","unstructured":"M. Engel et al. A formal approach to computer systems requirements documentation. In R. L. Grossman, A. Nerode, A. P. Ravn, and H. Rischel, editors, Hybrid Systems, volume 736 of LNCS, pages 452\u2013474, 1993.","DOI":"10.1007\/3-540-57318-6_40"},{"key":"15_CR18","doi-asserted-by":"crossref","unstructured":"M. Fr\u00c4nzle and M. M\u00fcller-Olm. Towards provably correct code generation for a hard real-time programming language. In P. A. Fritzson, editor, Compiler Construction '94, 5th International Conference, Edinburgh, UK, volume 786 of LNCS, pages 294\u2013308, 1994.","DOI":"10.1007\/3-540-57877-3_20"},{"key":"15_CR19","volume-title":"ProCoS Technical Report [Kiel MF 11\/3]","author":"M. Fr\u00c4nzle","year":"1993","unstructured":"M. Fr\u00c4nzle and B. von Karger. Proposal for a programming language core for ProCoS II. ProCoS Technical Report [Kiel MF 11\/3], Christian-Albrechts-Universit\u00c4t Kiel, Germany, August 1993."},{"key":"15_CR20","doi-asserted-by":"crossref","unstructured":"C. Ghezzi, D. Mandrioli, and A. Morzenti. TRIO: A logic language for executable specifications of real-time systems. Journal of Systems and Software, May 1990.","DOI":"10.1016\/0164-1212(90)90074-V"},{"key":"15_CR21","doi-asserted-by":"crossref","unstructured":"D. I. Good and W. D. Young. Mathematical methods for digital system development. In S. Prehn and W. J. Toetenel, editors, VDM '91, Formal Software Development Methods: Volume 2, volume 552 of LNCS, pages 406\u2013430, 1991.","DOI":"10.1007\/BFb0020002"},{"key":"15_CR22","doi-asserted-by":"crossref","unstructured":"M. R. Hansen and Zhou Chaochen. Semantics and completeness of the Duration Calculus. In J. W. de Bakker, K. Huizing, W.-P. de Roever, and G. Rozenberg, editors, Real-Time: Theory in Practice, volume 600 of LNCS, pages 209\u2013225, 1992.","DOI":"10.1007\/BFb0031994"},{"key":"15_CR23","doi-asserted-by":"crossref","first-page":"231","DOI":"10.1016\/0167-6423(87)90035-9","volume":"8","author":"D. Harel","year":"1987","unstructured":"D. Harel. Statecharts: A visual formalism for complex systems. Science of Computer Programming, 8:231\u2013274, 1987.","journal-title":"Science of Computer Programming"},{"key":"15_CR24","doi-asserted-by":"crossref","unstructured":"He Jifeng and J. P. Bowen. Time interval semantics and implementation of a real-time programming language. In Proc. 4th Euromicro Workshop on Real-Time Systems, pages 110\u2013115. IEEE Computer Society Press, 1992.","DOI":"10.1109\/EMWRT.1992.637480"},{"key":"15_CR25","doi-asserted-by":"crossref","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 Verification Methods, volume 683 of LNCS, pages 214\u2013225. Springer-Verlag, 1993.","DOI":"10.1007\/BFb0021726"},{"key":"15_CR26","unstructured":"C. A. R. Hoare. Communicating Sequential Processes. Prentice Hall International Series in Computer Science, 1985."},{"key":"15_CR27","unstructured":"C. A. R. Hoare. Refinement algebra proves correctness of compiling specifications. In C. C. Morgan and J. C. P. Woodcock, editors, 3rd Refinement Workshop, Workshops in Computer Science, pages 33\u201348. Springer-Verlag, 1991."},{"issue":"8","key":"15_CR28","doi-asserted-by":"crossref","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. S\u00d8rensen, 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":"15_CR29","doi-asserted-by":"crossref","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":"15_CR30","doi-asserted-by":"crossref","unstructured":"J. Hooman and J. Widom. A temporal-logic based compositional proof system for real-time message passing. In PARLE '89, Parallel Architectures and Languages Europe: Volume II, volume 366 of LNCS, pages 424\u2013441. Springer, 1989.","DOI":"10.1007\/3-540-51285-3_56"},{"key":"15_CR31","doi-asserted-by":"crossref","unstructured":"R. Inal. Modular specification of real-time systems. In Proc. 6th Euromicro Workshop on Real-Time Systems, pages 16\u201321. IEEE Computer Society Press, 1994.","DOI":"10.1109\/EMWRTS.1994.336871"},{"key":"15_CR32","unstructured":"INMOS Limited. Occam 2 Reference Manual. Prentice Hall, 1988."},{"key":"15_CR33","unstructured":"INMOS limited. Transputer Instruction Set: A Compiler Writer's Guide. Prentice Hall, first edition, 1988."},{"issue":"3","key":"15_CR34","doi-asserted-by":"crossref","first-page":"241","DOI":"10.1109\/32.75414","volume":"17","author":"M. S. Jaffe","year":"1991","unstructured":"M. S. Jaffe, N. G. Leveson, M. P. Heimdahl, and B. E. Melhart. Software requirements analysis for real-time process-control systems. IEEE Trans. Software Engineering, 17(3):241\u2013258, March 1991.","journal-title":"IEEE Trans. Software Engineering"},{"key":"15_CR35","unstructured":"J. J. Joyce. Totally verified systems: Linking verified software to verified hardware. In M. Leeser and G. Brown, editors, Hardware Specification, Verification and Synthesis: Mathematical Aspects, volume 408 of LNCS, pages 277\u2013201, 1990."},{"issue":"4","key":"15_CR36","doi-asserted-by":"crossref","first-page":"255","DOI":"10.1007\/BF01995674","volume":"2","author":"R. Koymans","year":"1990","unstructured":"R. Koymans. Specifying real-time properties with metric temporal logic. Real-Time Systems, 2(4):255\u2013299, November 1990.","journal-title":"Real-Time Systems"},{"key":"15_CR37","doi-asserted-by":"crossref","unstructured":"B. Krieg-Br\u00fcckner. Algebraic specification and functionals for transformational program and meta program development. In J. Diaz and F. Orejas, editors, Proc. TAPSOFT '89: Volume 2, volume 352 of LNCS, 1989.","DOI":"10.1007\/3-540-50940-2_26"},{"key":"15_CR38","volume-title":"Technical report","author":"L. Lamport","year":"1991","unstructured":"L. Lamport. The temporal logic of actions. Technical report, Digital Systems Research Center, 130 Lytton Avenue, Palo Alto, California 94301, USA, 25 December 1991."},{"key":"15_CR39","doi-asserted-by":"crossref","unstructured":"L. Lamport. Hybrid systems in TLA+. In R. L. Grossman, A. Nerode, A. P. Ravn, and H. Rischel, editors, Hybrid Systems, volume 736 of LNCS, pages 77\u2013102, 1993.","DOI":"10.1007\/3-540-57318-6_25"},{"issue":"2","key":"15_CR40","doi-asserted-by":"crossref","first-page":"34","DOI":"10.1145\/102792.102799","volume":"34","author":"N. Leveson","year":"1991","unstructured":"N. Leveson. Software safety in embedded computer systems. Communications of the ACM, 34(2):34\u201346, February 1991.","journal-title":"Communications of the ACM"},{"key":"15_CR41","doi-asserted-by":"crossref","unstructured":"N. A. Lynch and M. R. Tuttle. Hierarchical correctness proofs for distributed algorithms. In Proc. 6th PODC, pages 137\u2013151, 1987.","DOI":"10.1145\/41840.41852"},{"key":"15_CR42","doi-asserted-by":"crossref","unstructured":"Z. Manna and A. Pnueli. The Temporal Logic of Reactive and Concurrent Systems. Springer-Verlag, 1992.","DOI":"10.1007\/978-1-4612-0931-7"},{"key":"15_CR43","unstructured":"A. J. Martin. The design of a delay-insensitive microprocessor: An example of circuit synthesis by program transformation. In M. Leeser and G. Brown, editors, Hardware Specification, Verification and Synthesis: Mathematical Aspects, volume 408 of LNCS, pages 244\u2013259, 1990."},{"key":"15_CR44","unstructured":"A. J. Martin. Programming in VLSI: From communicating processes into delay-insensitive circuits. In C. A. R. Hoare, editor, Developments in Concurrency and Communication, University of Texas at Austin Year of Programming Series, chapter 1. Addison-Wesley, 1990."},{"key":"15_CR45","volume-title":"ProCoS Technical Report [ID\/DTH PCM 1\/1]","author":"P. C. Masiero","year":"1993","unstructured":"P. C. Masiero, A. P. Ravn, and H. Rischel. Refinement of real-time specifications. ProCoS Technical Report [ID\/DTH PCM 1\/1], Department of Computer Science, Technical University of Denmark, DK-2800 Lyngby, Denmark, July 1993."},{"key":"15_CR46","doi-asserted-by":"crossref","unstructured":"D. May. Occam and the Transputer. In C. A. R. Hoare, editor, Developments in Concurrency and Communication, University of Texas at Austin Year of Programming Series, chapter 2. Addison-Wesley, 1990.","DOI":"10.1007\/3-540-52494-0_36"},{"key":"15_CR47","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":"15_CR48","unstructured":"R. Milner. Communication and Concurrency. Prentice Hall International Series in Computer Science, 1989."},{"key":"15_CR49","unstructured":"Robin Milner, Mads Tofte, and Robert Harper. The Definition of Standard ML. The MIT Press, 1990."},{"key":"15_CR50","doi-asserted-by":"crossref","first-page":"243","DOI":"10.1016\/0020-0190(88)90147-0","volume":"26","author":"C. C. Morgan","year":"1988","unstructured":"C. C. Morgan. Data refinement by miracles. Information Processing Letters, 26:243\u2013246, 1988.","journal-title":"Information Processing Letters"},{"key":"15_CR51","unstructured":"C. C. Morgan. Programming From Specifications. Prentice Hall International Series in Computer Science, 1990."},{"key":"15_CR52","doi-asserted-by":"crossref","unstructured":"F. Lockwood Morris. Advice on structuring compilers and proving them correct. In Proc. ACM Symp. Principles of Programming Languages, Boston, Mass., pages 144\u2013152, 1973.","DOI":"10.1145\/512927.512941"},{"issue":"2","key":"15_CR53","doi-asserted-by":"crossref","first-page":"10","DOI":"10.1109\/MC.1985.1662795","volume":"18","author":"B. Moszkowski","year":"1985","unstructured":"B. Moszkowski. A temporal logic for multi-level reasoning about hardware. IEEE Computer, 18(2):10\u201319, 1985.","journal-title":"IEEE Computer"},{"key":"15_CR54","doi-asserted-by":"crossref","unstructured":"B. Moszkowski. Executing Temporal Logic Programs. Cambridge University Press, 1986.","DOI":"10.1007\/3-540-15670-4_6"},{"key":"15_CR55","volume-title":"ProCoS Technical Report [Kiel MMO 6\/2]","author":"M. M\u00fcller-Olm","year":"1993","unstructured":"M. M\u00fcller-Olm. On translation of TimedPL and capture of machine instruction timing. ProCoS Technical Report [Kiel MMO 6\/2], Christian-Albrechts-Universit\u00c4t Kiel, Germany, August 1993."},{"key":"15_CR56","volume-title":"ProCoS Technical Report Kiel MMO 10\/1","author":"M. M\u00fcller-Olm","year":"1994","unstructured":"Markus M\u00fcller-Olm. A new proposal for TimedPL's semantics. ProCoS Technical Report Kiel MMO 10\/1, Christian-Albrechts-Universit\u00c4t Kiel, Germany, May 1994."},{"key":"15_CR57","doi-asserted-by":"crossref","unstructured":"E.-R. Olderog. Nets, Terms and Formulas. Cambridge University Press, 1991.","DOI":"10.1017\/CBO9780511526589"},{"key":"15_CR58","doi-asserted-by":"crossref","unstructured":"E.-R. Olderog. Towards a design calculus for communicating programs. In J. C. M. Baeten and J. F. Groote, editors, Proc. CONCUR '91, volume 527 of LNCS, pages 61\u201372, 1991.","DOI":"10.1007\/3-540-54430-5_81"},{"key":"15_CR59","doi-asserted-by":"crossref","unstructured":"E.-R. Olderog. Interfaces between languages for communicating systems. In W. Kuich, editor, Automata, Languages and Programming, volume 623 of LNCS, 1992.","DOI":"10.1007\/3-540-55719-9_111"},{"key":"15_CR60","doi-asserted-by":"crossref","unstructured":"E.-R. Olderog and S. R\u00f6ssig. A case study in transformational design of concurrent systems. In M.-C. Gaudel and J.-P. Jouannaud, editors, TAPSOFT '93: Theory and Practice of Software Development, volume 668 of LNCS, pages 90\u2013104, 1993.","DOI":"10.1007\/3-540-56610-4_58"},{"key":"15_CR61","volume-title":"Technical Report Bericht 3\/92","author":"E.-R. Olderog","year":"1992","unstructured":"E.-R. Olderog, S. R\u00f6ssig, J. Sander, and M. Schenke. ProCoS at Oldenburg: The interface between specification language and Occam-like programming language. Technical Report Bericht 3\/92, Univ. Oldenburg, Fachbereich Informatik, Germany, 1992."},{"key":"15_CR62","first-page":"271","volume-title":"FPGAs, Oxford Workshop on Field Programmable Logic and Applications","author":"I. Page","year":"1991","unstructured":"I. Page and W. Luk. Compiling Occam into field programmable gate arrays. In FPGAs, Oxford Workshop on Field Programmable Logic and Applications, pages 271\u2013284, 15 Harcourt Way, Abingdon OX14 1NV, UK, 1991. Abingdon EE&CS Books."},{"issue":"2","key":"15_CR63","doi-asserted-by":"crossref","first-page":"251","DOI":"10.1109\/TSE.1986.6312940","volume":"12","author":"D. L. Parnas","year":"1986","unstructured":"D. L. Parnas and P. C. Clements. A rational design process: How and why to fake it. IEEE Trans. Software Engineering, 12(2):251\u2013257, February 1986.","journal-title":"IEEE Trans. Software Engineering"},{"key":"15_CR64","volume-title":"Technical Report CRL 237","author":"D. L. Parnas","year":"1991","unstructured":"D. L. Parnas and J. Madey. Functional documentation for computer systems engineering (version 2). Technical Report CRL 237, TRIO, McMaster University, Hamilton, Canada, September 1991."},{"key":"15_CR65","doi-asserted-by":"crossref","unstructured":"A. Pnueli and E. Harel. Applications of temporal logic to the specification of real-time systems (extended abstract). In M. Joseph, editor, Formal Techniques in Real-Time and Fault-Tolerant Systems, volume 331 of LNCS, pages 84\u201398. Springer, 1988.","DOI":"10.1007\/3-540-50302-1_4"},{"key":"15_CR66","unstructured":"A. P. Ravn and H. Rischel. Requirements capture for embedded real-time systems. In Proc. IMACS-MCTS'91 Symp. on Modelling and Control of Technological Systems, volume 2, pages 147\u2013152. IMACS, May 1991."},{"issue":"1","key":"15_CR67","doi-asserted-by":"crossref","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 Trans. Software Engineering, 19(1):41\u201355, January 1993.","journal-title":"IEEE Trans. Software Engineering"},{"key":"15_CR68","doi-asserted-by":"crossref","first-page":"177","DOI":"10.1016\/0304-3975(88)90049-7","volume":"60","author":"A. W. Roscoe","year":"1988","unstructured":"A. W. Roscoe and C. A. R. Hoare. Laws of Occam programming. Theoretical Computer Science, 60:177\u2013229, 1988.","journal-title":"Theoretical Computer Science"},{"key":"15_CR69","doi-asserted-by":"crossref","unstructured":"S. R\u00f6ssig and M. Schenke. Specification and stepwise development of communicating systems. In S. Prehn and W. J. Toetenel, editors, VDM '91, Formal Software Development Methods: Volume 1, volume 551 of LNCS, pages 149\u2013163, 1991.","DOI":"10.1007\/3-540-54834-3_11"},{"key":"15_CR70","doi-asserted-by":"crossref","unstructured":"M. Schenke. Specification and transformation of reactive systems with time restrictions and concurrency. In these proceedings, 1994.","DOI":"10.1007\/3-540-58468-4_186"},{"key":"15_CR71","doi-asserted-by":"crossref","unstructured":"J. U. Skakkeb\u00c6k, A. P. Ravn, H. Rischel, and Zhou Chaochen. Specification of embedded, real-time systems. In Proc. 4th Euromicro Workshop on Real-Time Systems, pages 116\u2013121. IEEE Computer Society Press, 1992.","DOI":"10.1109\/EMWRT.1992.637481"},{"key":"15_CR72","doi-asserted-by":"crossref","unstructured":"J. U. Skakkeb\u00c6k and N. Shankar. Towards a Duration Calculus proof assistant in PVS. In these proceedings, 1994.","DOI":"10.1007\/3-540-58468-4_189"},{"key":"15_CR73","unstructured":"J. M. Spivey. The Z Notation: A Reference Manual. Prentice Hall International Series in Computer Science, 2nd edition, 1992."},{"key":"15_CR74","doi-asserted-by":"crossref","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\u2013245, 1981.","journal-title":"Theoretical Computer Science"},{"issue":"4","key":"15_CR75","doi-asserted-by":"crossref","first-page":"453","DOI":"10.1093\/logcom\/1.4.453","volume":"1","author":"Y. Venema","year":"1991","unstructured":"Y. Venema. A modal logic for chopping intervals. J. Logic of Computation, 1(4):453\u2013476, 1991.","journal-title":"J. Logic of Computation"},{"key":"15_CR76","unstructured":"A. Wikstr\u00f6m. Functional Programming using Standard ML. Prentice Hall International Series in Computer Science, first edition, 1987."},{"key":"15_CR77","doi-asserted-by":"crossref","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 (1986) 121\u2013126.","journal-title":"Proc. Cambridge Phil. Soc."},{"key":"15_CR78","volume-title":"Technical report","author":"Xilinx Inc.","year":"1991","unstructured":"Xilinx Inc. The programmable gate array data book. Technical report, Xilinx Inc., San Jose, California, USA, 1991."},{"issue":"1","key":"15_CR79","first-page":"49","volume":"1","author":"Z. Liu","year":"1994","unstructured":"Zhiming Liu, A. P. Ravn, E. V. S\u00d8rensen, and Zhou Chaochen. Towards a calculus of systems dependability. High Integrity Systems, 1(1):49\u201375, January 1994.","journal-title":"High Integrity Systems"},{"key":"15_CR80","doi-asserted-by":"crossref","unstructured":"Zhou Chaochen. Duration Calculi: An overview. In D. Bj\u00d8rner, M. Broy, and I. V. Pottosin, editors, Formal Methods in Programming and their Application, volume 735 of LNCS, pages 256\u2013266, 1993.","DOI":"10.1007\/BFb0039713"},{"key":"15_CR81","doi-asserted-by":"crossref","unstructured":"Zhou Chaochen, M. R. Hansen, and P. Sestoft. Decidability results for Duration Calculus. In P. Enjalbert, A. Finkel, and K. W. Wagner, editors, Proc. STACS 93, volume 665 of LNCS, pages 58\u201368, 1993.","DOI":"10.1007\/3-540-56503-5_8"},{"key":"15_CR82","doi-asserted-by":"crossref","unstructured":"Zhou Chaochen, C. A. R. Hoare, and A. P. Ravn. A calculus of durations. Information Processing Letters, 40(5), December 1991.","DOI":"10.1016\/0020-0190(91)90122-X"},{"key":"15_CR83","doi-asserted-by":"crossref","unstructured":"Zhou Chaochen, A. P. Ravn, and M. R. Hansen. An extended Duration Calculus for hybrid real-time systems. In R. L. Grossman, A. Nerode, A. P. Ravn, and H. Rischel, editors, Hybrid Systems, volume 736 of LNCS, pages 36\u201359, 1993.","DOI":"10.1007\/3-540-57318-6_23"},{"key":"15_CR84","unstructured":"J. Zwiers. Compositionality, Concurrency, and Partial Correctness: Proof Theories for Networks of Processes and their Relationship, volume 321 of LNCS. Springer-Verlag, 1989."}],"container-title":["Lecture Notes in Computer Science","Formal Techniques in Real-Time and Fault-Tolerant Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-58468-4_171.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,6,20]],"date-time":"2023-06-20T18:44:55Z","timestamp":1687286695000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-58468-4_171"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1994]]},"ISBN":["9783540584681","9783540489849"],"references-count":84,"URL":"https:\/\/doi.org\/10.1007\/3-540-58468-4_171","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1994]]}}}