{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T22:33:16Z","timestamp":1725489196836},"publisher-location":"Berlin, Heidelberg","reference-count":36,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540417910"},{"type":"electronic","value":"9783540452515"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2001]]},"DOI":"10.1007\/3-540-45251-6_17","type":"book-chapter","created":{"date-parts":[[2007,8,12]],"date-time":"2007-08-12T01:53:28Z","timestamp":1186883608000},"page":"300-317","source":"Crossref","is-referenced-by-count":0,"title":["Real-Time Logic Revisited"],"prefix":"10.1007","author":[{"given":"Stephen E.","family":"Paynter","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2001,3,16]]},"reference":[{"key":"17_CR1","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/BFb0031985","volume-title":"Proc. REX Workshop-Real-Time: Theory in Practice","author":"M. Abadi","year":"1991","unstructured":"Abadi, M. and Lamport, L.: \u2018An Old Fashioned Recipe for Real-Time\u2019, Proc. REX Workshop-Real-Time: Theory in Practice, LNCS 600, Springer, 1991, pp. 1\u201327."},{"issue":"2","key":"17_CR2","doi-asserted-by":"publisher","first-page":"143","DOI":"10.1007\/BF00360339","volume":"10","author":"J.M. Armstrong","year":"1996","unstructured":"Armstrong, J.M. and Barroca, L.: \u2018Specification and Verification of Reactive System Behaviour: The Railroad Crossing Example\u2019, J. Real-Time Systems, 10(2), March 1996, pp. 143\u2013178.","journal-title":"J. Real-Time Systems"},{"key":"17_CR3","doi-asserted-by":"publisher","first-page":"211","DOI":"10.1016\/S0164-1212(97)00168-4","volume":"40","author":"J.M. Armstrong","year":"1998","unstructured":"Armstrong, J.M.: \u2018Industrial Integration of Graphical Formal Specifications\u2019, J. Systems Software, 40, 1998, pp. 211\u2013225.","journal-title":"J. Systems Software"},{"key":"17_CR4","unstructured":"Armstrong, J.M.: \u2018The Proofcharts-PVS Manual-Part II: The Proofcharts-PVS Theorem Library\u2019, BAE SYSTEMS DCSC Technical Report, DCSC\/TR\/1999\/5, University of Newcastle, 1999."},{"key":"17_CR5","series-title":"Lect Notes Comput Sci","volume-title":"Proc. 2nd Int. Symp. on Formal Techniques in Real-Time and Fault-Tolerant Systems","author":"C.J. Fidge","year":"1992","unstructured":"Fidge, C.J.: \u2018Specification and Verification of Real-Time Behaviour Using Z and RTL\u2019, Proc. 2nd Int. Symp. on Formal Techniques in Real-Time and Fault-Tolerant Systems, LNCS 571, Springer, 1992."},{"key":"17_CR6","series-title":"Lect Notes Comput Sci","volume-title":"Formal Analysis of a Real-Time Kernel Specification","author":"S. Fowler","year":"1996","unstructured":"Fowler, S. and Wellings, A.J.: \u2018Formal Analysis of a Real-Time Kernel Specification\u2019, Proc. 4\n                        th Int. Symp. on Formal Techniques in Real-Time and Fault-Tolerant Systems, LNCS 1135, Springer, 1996."},{"key":"17_CR7","doi-asserted-by":"crossref","unstructured":"Fowler, S. and Wellings, A.J.: \u2018Formal Development of a Real-Time Kernel\u2019, Proc. 18th IEEE Real-Time Systems Symp., San Francisco, December 1997.","DOI":"10.1109\/REAL.1997.641284"},{"key":"17_CR8","doi-asserted-by":"publisher","first-page":"173","DOI":"10.1007\/BF01700692","volume":"38","author":"K. G\u00f6del","year":"1931","unstructured":"G\u00f6del, K.: \u2018\u00dcber formal unentscheidbare S\u00e4tze der Principia Mathematica and verwandter Systeme I\u2019, In Monatshefte f\u00fcr Mathematik and Physik, Vol. 38, pp. 173\u2013198, 1931. Reprinted in Translation in \u2018On Formally Undecidable Propositions of Principia Mathematica and Related Systems\u2019, Dover Publications, 1992.","journal-title":"In Monatshefte f\u00fcr Mathematik and Physik"},{"key":"17_CR9","unstructured":"Hall, J.G. and Lemos, R. de.: \u2018ERTL: An Extension to RTL for the Specification, Analysis and Verification of Hybrid Systems\u2019, Proc. of the IEEE EuroMirco\u201996 Conf., 1996."},{"key":"17_CR10","first-page":"279","volume-title":"Time and Logic: A Computational Approach","author":"E. Hajnicz","year":"1995","unstructured":"Hajnicz, E.: \u2018An Analysis of Structure of Time in the First Order Predicate Calculus\u2019, In L. Bolc and A. Szalas (Editors): \u2018Time and Logic: A Computational Approach\u2019, UCL Press (London), 1995, pp. 279\u2013322."},{"key":"17_CR11","unstructured":"Haveman, J.: \u2018Transaction Decomposition: Refinement of Timing Con-straints\u2019, Proc. of the South Pacific Conf. on Formal Methods, 1997."},{"issue":"9","key":"17_CR12","doi-asserted-by":"crossref","first-page":"890","DOI":"10.1109\/TSE.1986.6313045","volume":"12","author":"F. Jahanian","year":"1986","unstructured":"Jahanian, F., and Mok, A.K.: \u2018Safety Analysis of Timing Properties in Real-Time Systems\u2019, IEEE Trans. on Soft. Eng., 12(9), 1986, pp. 890\u2013904.","journal-title":"IEEE Trans. on Soft. Eng."},{"issue":"18","key":"17_CR13","doi-asserted-by":"publisher","first-page":"961","DOI":"10.1109\/TC.1987.5009519","volume":"36","author":"F. Jahanian","year":"1987","unstructured":"Jahanian, F., and Mok, A.K.: \u2018A Graph-Theoretic Approach for Timing Analysis and its Implementation\u2019, IEEE Trans. on Comp., 36(18), 1987, pp. 961\u2013975.","journal-title":"IEEE Trans. on Comp."},{"issue":"12","key":"17_CR14","doi-asserted-by":"publisher","first-page":"933","DOI":"10.1109\/32.368134","volume":"20","author":"F. Jahanian","year":"1994","unstructured":"Jahanian, F., and Mok, A.K.: \u2018Modechart: A Specification Language for Real-Time Systems\u2019, IEEE Trans. on Soft. Eng., 20(12), 1994, pp. 933\u2013947.","journal-title":"IEEE Trans. on Soft. Eng."},{"key":"17_CR15","unstructured":"Jahanian, F., Lee, R. and Mok, A.K.: \u2018Semantics of Modechart in Real-Time Logic\u2019, IEEE Proc. of the 21st Annual Hawaiian Int. Conf. on System Science, 1988."},{"key":"17_CR16","series-title":"Technical Report TR-88-25, Department of Computer Science","volume-title":"Formal Specification of Real-time Systems","author":"F. Jahanian","year":"1988","unstructured":"Jahanian, F., Mok, A.K., and Stuart, D.A.: \u2018Formal Specification of Real-time Systems\u2019, Technical Report TR-88-25, Department of Computer Science, University of Texas at Austin, June 1988."},{"key":"17_CR17","unstructured":"Kleene, S.C.: \u2018Introduction to Metamathematics\u2019, North-Holland Publishing Company, 1952."},{"key":"17_CR18","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"488","DOI":"10.1007\/3-540-58468-4_180","volume-title":"Proc. 3rd Int. Symp. on Formal Techniques in RealTime and Fault-Tolerant Systems","author":"Y. Lakhneche","year":"1994","unstructured":"Lakhneche, Y. and Hooman, J.: \u2018Reasoning about Durations in Metric Temporal Logic\u2019, Proc. 3rd Int. Symp. on Formal Techniques in RealTime and Fault-Tolerant Systems, LNCS 863, Springer-Verlag, 1994, pp. 488\u2013510."},{"key":"17_CR19","doi-asserted-by":"publisher","first-page":"77","DOI":"10.1007\/BF01786227","volume":"1","author":"L. L","year":"1986","unstructured":"Lamport, L.: \u2018On Interprocess Communication-Part 1: Basic Formalism\u2019, Distributed Comp. 1, 1986, pp. 77\u201385.","journal-title":"Distributed Comp"},{"key":"17_CR20","unstructured":"Lemos, R. de. and Hall, J.G.: \u2018Extended RTL in the Specification and Verification of an Industrial Press\u2019, Proc. of DIMAC\u201995 Conf., 1995."},{"key":"17_CR21","unstructured":"Liu, Z.: \u2018Specification and Verification in the Duration Calculus\u2019, Chapter 7 of M. Joseph (Editor): \u2018Real-Time Systems: Specification, Verification, and Analysis\u2019, Prentice-Hall International Series in Computer Science, 1996."},{"issue":"7","key":"17_CR22","doi-asserted-by":"publisher","first-page":"609","DOI":"10.1007\/BF01191722","volume":"30","author":"Z. Manna","year":"1993","unstructured":"Manna, Z. and Pnueli, A.: \u2018Models of Reactivity\u2019, Acta Informatica, 30(7), 1993, pp. 609\u2013678.","journal-title":"Acta Informatica"},{"key":"17_CR23","unstructured":"Manzano, M.: \u2018Introduction to Many-Sorted Logic\u2019, in \u2018Many-Sorted Logic and its Applications\u2019, Edited by K. Meinke and J.V. Tucker, Wiley Professional Computing, 1993"},{"key":"17_CR24","unstructured":"Manzano, M.: \u2018Extensions of First-Order Logic\u2019, Tracts in Theoretical Computer Science, Cambridge University Press, 1996"},{"key":"17_CR25","series-title":"Lect Notes Comput Sci","volume-title":"Proc. 2nd Int. Symp. on Formal Techniques in Real-Time and Fault-Tolerant Systems","author":"O. Millet","year":"1992","unstructured":"Millet, O.: \u2018Multicycles and RTL Logic Satisfiability\u2019, Proc. 2nd Int. Symp. on Formal Techniques in Real-Time and Fault-Tolerant Systems, LNCS 571, Springer, 1992."},{"key":"17_CR26","unstructured":"Mok, A.K., Stuart, D.A., and Jahanian, F.: \u2018Specification and Analysis of Real-Time Systems: Modechart Language and Toolset\u2019, Chapter in Heitmeyer, C. and Mandrioli, D. (Editors): \u2018Formal Methods for Real-Time Computing\u2019, Trends in Software 5, Wiley, 1996."},{"key":"17_CR27","unstructured":"Owre, S., Shanker, N., Rushby, J.M., and Stringer-Calvert, D.W.J.: \u2018PVS Language: Version 2.3\u2019, Computer Science Laboratory, SRI International, September 1999."},{"key":"17_CR28","unstructured":"Owre, S., Shanker, N., Rushby, J.M., and Stringer-Calvert, D.W.J.: \u2018PVS System Guide: Version 2.3\u2019, Computer Science Laboratory, SRI International, September 1999."},{"key":"17_CR29","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0055336","volume-title":"Proc. 5th Int. Symp. on Formal Techniques in Real-Time and Fault-Tolerant Systems","author":"P.K. Pandya","year":"1998","unstructured":"Pandya, P.K. and Hung, D.V.: \u2018Duration Calculus of Weakly Monotonic Time\u2019, Proc. 5th Int. Symp. on Formal Techniques in Real-Time and Fault-Tolerant Systems, LNCS 1486, Springer, 1998."},{"key":"17_CR30","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"90","DOI":"10.1007\/3-540-61648-9_36","volume-title":"Proc. 4th Int. Symp. on Formal Techniques in Real-Time and Fault-Tolerant Systems","author":"S.E. Paynter","year":"1996","unstructured":"Paynter, S.E.: \u2018Real-Time Mode-Machines\u2019, Proc. 4th Int. Symp. on Formal Techniques in Real-Time and Fault-Tolerant Systems, LNCS 1135, Springer, 1996, pp. 90\u2013109."},{"key":"17_CR31","unstructured":"Paynter, S.E.: \u2018Real-Time Transactions Revisited\u2019, Unclassified MBD(UK) Technical Report, DR16972, 1999."},{"issue":"2","key":"17_CR32","doi-asserted-by":"publisher","first-page":"120","DOI":"10.1007\/s001650070032","volume":"12","author":"S.E. Paynter","year":"2000","unstructured":"Paynter, S.E., Armstrong, J.M., and Haveman, J.: \u2018ADL: An Activity Description Language for Real-Time Networks\u2019, Formal Aspects of Comp., 12(2),2000, pp. 120\u2013144.","journal-title":"Formal Aspects of Comp."},{"key":"17_CR33","doi-asserted-by":"publisher","first-page":"468","DOI":"10.2307\/421132","volume":"1","author":"M. Rathjen","year":"1995","unstructured":"Rathjen, M.: \u2018Recent Advances in Ordinal Analysis: \u041f1\n                        2 \u2014CA and Related Systems\u2019, Bulletin of Symbolic Logic, 1, 1995, pp. 468\u2013485.","journal-title":"Bulletin of Symbolic Logic"},{"key":"17_CR34","series-title":"Lect Notes Comput Sci","volume-title":"Proc. 3rd Int. Symp. on Formal Techniques in Real-Time and Fault-Tolerant Systems","author":"J.U. Skakkebaek","year":"1994","unstructured":"Skakkebaek, J.U. and Shankar, N.: \u2018Towards a Duration Calculus Proof Assistant in PVS\u2019, Proc. 3rd Int. Symp. on Formal Techniques in Real-Time and Fault-Tolerant Systems, LNCS 863, Springer-Verlag, 1994."},{"key":"17_CR35","unstructured":"Simpson, H.R.: \u2018Protocols for Process Interaction\u2019, Submitted to IEE Proc. on Soft. Eng., Also three MBD(UK) Technical Reports, 2000."},{"key":"17_CR36","doi-asserted-by":"publisher","first-page":"269","DOI":"10.1016\/0020-0190(91)90122-X","volume":"40","author":"C. Zhou","year":"1991","unstructured":"Zhou, C. Hoare, C.A.R., and Ravn, A.P.: \u2018A Calculus of Durations\u2019, Inform. Proc. Letters, 40, 1991, pp. 269\u2013276.","journal-title":"Inform. Proc. Letters"}],"container-title":["Lecture Notes in Computer Science","FME 2001: Formal Methods for Increasing Software Productivity"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-45251-6_17","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,2,21]],"date-time":"2019-02-21T14:42:58Z","timestamp":1550760178000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45251-6_17"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2001]]},"ISBN":["9783540417910","9783540452515"],"references-count":36,"URL":"https:\/\/doi.org\/10.1007\/3-540-45251-6_17","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2001]]}}}