Abstract
Duration Calculus (DC) is an interval logic which was introduced to express and reason about models of real-time systems. DC was introduced by Zhou Chaochen, Tony Hoare and A.P. Ravn during the ProCoS I Project (ESPRIT BRA 3104, 1989–1991) [6]. Formal techniques for the construction of safetycritical systems were investigated in this project, and in an early case study of gas burner systems, conducted by E.V. Sørensen, A.P. Ravn and H. Rischel, it turned out that certain requirements for such systems were not expressible in the real-time formalisms which were available at that time.
This work is partially funded by The Danish Council for Strategic Research under project MoDES.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
J.F. Allen (1983) Maintaining Knowledge about Temporal Intervals. Communications of the ACM 26(11):832–843, 1983
J.F. Allen (1984) Towards a general theory of action and time. Artificial Intelligence 23:123–154
R. Alur, C. Courcoubetis, T. Henzinger, P.H. Ho (1993) Hybrid automata: An algorithmic approach to the specification and verification of hybrid systems. In Hybrid Systems, LNCS 736, Springer, Berlin Heidelberg New York: 209–229
R. Alur, D. Dill (1992) The theory of timed automata. In Real-Time: Theory in Practice, LNCS 600, Springer, Berlin Heidelberg New York: 45–73
R. Barua, S. Roy, and C. Zhou (2000) Completeness of neighbourhood logic. Journal of Logic and Computation 10(2): 271–295
D. Bjørner (1992) Trusted computing systems: the ProCoS experience. In Proceedings of the 14th international conference on Software engineering, Melbourne, Australia, ACM Press: 15–34
P. Blackburn, M. de Rijke, Y. Venema (2001) Modal Logic. Cambridge University Press
T. Bolander, J.U. Hansen, M.R. Hansen (2006) Decidability of hybrid duration calculus. In InternationalWorkshop on Hybrid Logics, Seattle 2006. To appear in Electronic Notes in Theoretical Computer Science.
V.A. Braberman, D.V. Hung (1998) On checking timed automata for linear duration invariants. In Proceedings of the 19th IEEE Real-Time Systems Symposium, IEEE Computer Society Press: 264–273
D. Basin, S. Matthews, L. Vigano (1997) Labelled propositional modal logics: theory and practice. Journal of logic and computation 7(6):685–717
D. Basin, S. Matthews, L. Vigano(1998) Labelled modal logics: quantifiers. Journal of logic, language and information 7(3):237–263
J.R. Buchi (1960) Weak second-order arithmetic and finite automata. Zeitschrift für Mathematische Logik und Grundlagen der Mathematik. 6:66–92
P. Chan, D.V. Hung (1995) Duration calculus specification of scheduling for tasks with shared resources. In Asian Computing Science Conference 1995, LNCS 1023, Springer, Berlin Heidelberg New York: 365–380
Z. Chen, J. Wang, C. Zhou (1995) An abstraction of hybrid control systems. In IEEE Singapore Intl. Conf. on Intelligent Control and Instrumentation. IEEE Press:1–6
S. Colin, G. Mariano, V. Poirriez (2004) Duration Calculus: A Real-Time Semantics for B. In Theoretical Aspects of Computing — ICTAC 2004, LNCS 3407, Springer, Berlin Heidelberg New York: 431–446
S. Dong, Q. Xu, N. Zhan (1999) A formal proof of the rate monotonic scheduler. In Proceedings of the Sixth International Conference on Real-Time Computing Systems and Applications. IEEE Computer Society Press:500–507
B. Dutertre (1995) Complete proof systems for first order interval temporal logic. In Tenth Annual IEEE Symposium on Logic in Computer Science, IEEE Press:36–43
B. Dutertre (1995) On first order interval temporal logic. Technical report, Report No. CSD-TR-94-3, Department of Computer Science, Royal Holloway, University of London
C.C. Elgot (1961) Decision problems of finite automata design and related arithmetics. Transactions of the American Mathematical Society 98:21–52
M. Engel, M. Kubica, J. Madey, D.L. Parnas, A.P. Ravn, A.J. van Schouwen (1993) A formal approach to computer systems requirements documentation. In Hybrid Systems, LNCS 736, Springer, Berlin Heidelberg New York: 452–474
M. Engel, H. Rischel (1994) Dagstuhl-seminar specification problem-a duration calculus solution. Technical report, Department of Computer Science, Technical University of Denmark — Personal Communication
M. Fränzle, M.R. Hansen (2005) A Robust Interpretation of Duration Calculus. In Theoretical Aspects of Computing — ICTAC 2005, LNCS 3722, Springer, Berlin Heidelberg New York: 257–271
M. Fränzle, M.R. Hansen (2007) Deciding an Interval Logic with Accumulated Durations. In Tools and algorithms for the construction and analysis of systems — TACAS 2007, LNCS 4424, Springer, Berlin Heidelberg New York: 201–215
M. Fränzle (1996) Synthesizing controllers from duration calculus. In Formal Techniques in Real-Time and Fault-Tolerant Systems, LNCS 1135, Springer, Berlin Heidelberg New York:168–187
M. Fränzle (1997) Controller Design from Temporal Logic: Undecidability Need Not Matter. PhD Thesis Institut für Informatik und Praktische Mathematik der Christian-Albrechts-Universität Kiel
M. Fränzle (2002) Take it NP-easy: Bounded model construction for duration calculus. In Formal Techniques in Real-Time and Fault-Tolerant Systems, LNCS 2469, Springer, Berlin Heidelberg New York:245–264
V. Goranko, A. Montanari, G. Sciavicco (2004) A Road Map of Propositional Interval Temporal Logics and Duration Calculi. Journal of Applied Nonclassical Logics, Special issue on Interval Temporal Logics and Duration Calculi, 14(1–2):11–56
D.P. Guelev (1998) A calculus of durations on abstract domains: Completeness and extensions. Technical report 139, UNU/IIST (UN University, Inst. of Software Technologz)
D.P. Guelev (2000) Complete fragment of higher-order duration μ-calculus. In Foundations of Software Technology and Theoretical Computer Science (FST&TCS’2000), LNCS 1974, Springer, Berlin Heidelberg New York:264–276
D.V. Guelev, D.V. Hung (1999) On the completeness and decidability of duration calculus with iteration. In Advances in Computing Science, LNCS 1742, Springer, Berlin Heidelberg New York:139–150
D.V. Guelev, D.V. Hung (2002) Prefix and projection onto state in duration calculus. In Proceedings of Workshop on Theory and Practice of Timed Systems, Electronic Notes in Theoretical Computer Science
J. Halpern, B. Moskowski, Z. Manna (1983) A hardware semantics based on temporal intervals. In ICALP’83, LNCS 154, Springer, Berlin Heidelberg New York:278–291
J. Halpern, Y. Shoham (1986) A propositional modal logic of time intervals. In Proceedings of the First IEEE Symposium on Logic in Computer Science, IEEE Press:279–292
J. Halpern, Y. Shoham (1991) A propositional modal logic of time intervals. Journal of the ACM 33(4):935–962
K.M. Hansen, A.P. Ravn, V. Stavridou (1996) From safety analysis to formal specification. Technical report, Department of Information Technology, Technical University of Denmark
M.R. Hansen (1994) Model-checking discrete duration calculus. Formal Aspects of Computing 6A:826–845
M.R. Hansen, C. Zhou (1992) Semantics and completeness of duration calculus. In Real-Time: Theory in Practice, LNCS 600, Springer, Berlin Heidelberg New York:209–225
M.R. Hansen, C. Zhou (1997) Duration calculus: Logical foundations. Formal Aspects of Computing 9:283–330
M.R. Hansen, C. Zhou, J. Staunstrup(1992) A real-time duration semantics for circuits. In TAU’92: 1992 Workshop on Timing Issues in the Specification and Synthesis of Digital Systems, Princeton Univ., NJ. ACM/SIGDA
M.R. Hansen, P.K. Pandya, C. Zhou (1995) Finite divergence. Theoretical Computer Science 138:113–139
M.R. Hansen, R. Sharp (2003) Using interval logics for temporal analysis of security protocols. In First ACM Workshop on Formal Methods in Security Engineering (FMSE’03), ACM Press:24–31
D. Harel, O. Lichtenstein, A. Pnueli (1990) Explicit clock temporal logic. In Symposium on Logic in Computer Science, IEEE Press:402–413
J. Harrison (1998) Theorem Proving with the Real Numbers. Springer, Berlin Heidelberg New York
J. Hoenicke, E.R. Olderog (2002) CSP-OZ-DC: A combination of specification techniques for processes, data and time. Nordic Journal of Computing 9(4):301–334
G.E. Hughes, M.J. Crestwell (1968) An Introduction to Modal Logic. Routledge
G.E. Hughes, M.J Crestwell (1984) A Companion to Modal Logic. Methuen
Z. Huibiao, J.F. He (2000) A DC-based semantics for Verilog. In Proceedings of International Conference on Software: Theory and Practice. Publishing House of Electronics Industry:421–432
D.V. Hung (1998) Modelling and verification of biphase mark protocols in duration calculus using PVS/DC−. In Application of Concurrency to System Design (CSD’98), IEEE Computer Society Press:88–98
D.V. Hung, C. Zhou (1999) Probabilistic duration calculus for continuous time. Formal Aspects of Computing, 11(1):21–44
D.V. Hung, P.H. Giang (1996) A sampling semantics of duration calculus. In Formal Techniques for Real-Time and Fault Tolerant Systems, LNCS 1135. Springer, Berlin Heidelberg New York: 188–207
D.V. Hung, D.P. Guelev (1999) Completeness and decidability of a fragment of duration calculus with iteration. In Advances in Computing Science, LNCS 1742. Springer, Berlin Heidelberg New York:139–150
D.V. Hung, J. Wand (1996) On design of hybrid control systems using i/o automata models. In Foundations of Software Technology and Theoretical Computer Science, LNCS 1180. Springer, Berlin Heidelberg New York:156–167
R. Inal (1994) Modular specification of real-time systems. In 1994 Euromicro Workshop on Real-Time Systems. IEEE Computer Society Press
J.F. He (1994) From CSP to hybrid systems. In A Classical Mind: Essays in Honour of C.A.R. Hoare. Prentice Hall International:171–190
J.F. He, J. Bowen (1992) Time interval semantics and implementation of a real-time programming language. In 1992 Euromicro Workshop on Real-Time Systems. IEEE Computer Society Press
J.F. He, C.A.R. Hoare, M. Fränzle, M. Müller-Olm, E.R. Olderog, M. Schenke, M.R. Hansen, A.P. Ravn, H. Rischel (1994) Provably correct systems. In Formal Techniques in Real-Time and Fault-Tolerant Systems, LNCS 863. Springer, Berlin Heidelberg New York:288–335
J.F. He, Q. Xu (2000) Advanced features of the duration calculus. In Millennial Perspectives in Computer Science. Palgrave:133–146
W. He, C. Zhou (1995) A case study of optimization. The Computer Journal 38(9):734–746
K.T. Hong, D.V. Hung (2001) Formal design of hybrid control systems: Duration calculus approach. In Proceedings of the Twenty-Fifth Annual International Computer Software and Applications Conference. IEEE Computer Society Press:423–428
F. Jahanian, A.K.L Mok (1986) Safety analysis of timing properties in real-time systems. IEEE Transaction on Software Engineering 12(9)
J. Gao, Q. Xu (1997) Rigorous design of a fault diagnosis and isolation algorithm. In Proceedings of the Fifth International Workshop on Hybrid Systems
Y. Kesten, A. Pnueli, J. Sifakis, S. Yovine (1993) Integration graphs: A class of decidable hybrid systems. In Hybrid Systems, LNCS 736. Springer, Berlin Heidelberg New York:179–208
C. Kleuker (2000) Constraint Diagrams. PhD Thesis, Oldenburg University, Germany
N. Klarlund, A. Moller (2001) MONA Version 1.4: User Manual. BRICS, Department of Computer Science, University of Aarhus, Denmark
M. Kääramees (1995) Transformation of duration calculus specifications to DISCO language. Master’s Thesis, Automation and Systems Engineering, Tallinn Technical University, Estonia
M. Kääramees(1995) Transforming designs towards implementations. In 1995 Euromicro Workshop on Real-Time Systems, IEEE Computer Society Press:197–204
R. Koymans (1990) Specifying real-time properties with metric temporal logic. Real-Time Systems 2(4):255–299
L. Lamport (1993) Hybrid systems in tla+. In Hybrid Systems, LNCS 736. Springer p. 77–102
X. Li (1993) A Mean Value Calculus. PhD Thesis, Software Institute, Academia Sinica
X. Li, J. Wang (1996) Specifying optimal design of a steam-boiler system. In Formal Methods for Industrial Applications, LNCS 1165. Springer Berlin Heidelberg New York:359–378
X. Li, D.V. Hung (1996) Checking linear duration invariants by linear programming. In Concurrency and Parallelism, Programming, Networking, and Security, LNCS 1179. Springer Berlin Heidelberg New York:321–332
X. Li, D.V. Hung, T. Zheng T (1997) Checking hybrid automata for linear duration invariants. In Advances in Computing Science, LNCS 1997. Springer Berlin Heidelberg New York:166–180
L. Li, J.F. He (1999) A denotational semantics of timed rsl using duration calculus. In Proceedings of the Sixth International Conference on Real-Time Computing Systems and Applications. IEEE Computer Society Press:492–503
C.L. Liu, J.W. Layland (1973) Scheduling algorithm for multiprogramming in a hard real-time environment. Journal of the ACM 20(1):46–61
Z. Liu, A.P. Ravn, E.V. Sørensen, C. Zhou (1993) A probabilistic duration calculus. In Dependable Computing and Fault-Tolerant Systems Vol. 7: Responsive Computer Systems. Springer Berlin Heidelberg New York:30–52
Z. Liu, A.P. Ravn, E.V. Sørensen, C. Zhou (1994) Towards a calculus of systems dependability. High Integrity Systems 1(1):49–75
Z. Liu, J. Nordahl, E.V. Sørensen (1995) Composition and refinement of probabilistic real-time systems. In Mathematics of Dependable Systems, Oxford University Press:149–163
Z. Liu (1996) Specification and verification in DC. In Mathematics of Dependable Systems, International Series in Computer Science, Prentice Hall p.182–228
Z. Manna, A. Pnueli (1993) Verifying hybrid systems. In Hybrid Systems, LNCS 736. Springer, Berlin Heidelberg New York:4–35
X. Mao, Q. Xu, D.V. Hung, J. Wang (1996) Towards a proof assistant for interval logics. Technical report, UNU/IIST Report No. 77, UN University, International Institute for Software Technology, Macau
P.C. Masiero, A.P. Ravn, H. Rischel (1993) Refinement of real-time specifications. Technical Report ProCoS, Technical Report ID/DTH PCM 1/1, Department of Computer Science, Technical University of Denmark
C. Meadows (2001) A cost-based framework for analysis of denial-of-service in networks. Journal of Computer Security 9(1/2):143–164
C.A. Middelburg (1998) Truth of duration calculus formulae in timed frames. Fundamenta Informaticae Journal 36(2/3):235–263
S. Mørk, J.C. Godskesen, M.R. Hansen, R. Sharp (1996) A timed semantics for sdl. In Formal Description Techniques IX: Theory, application and tools. Chapman & Hall:295–309
B. Moszkowski (1985) A temporal logic for multilevel reasoning about hardware. IEEE Computer 18(2):10–19
B. Moszkowski (1995) Compositional reasoning about projected and infinite time. In Engineering of Complex Computer Systems, IEEE Computer Society Press:238–245
X. Nicollin, A. Olivero, J. Sifakis, S. Yovine (1993) An approach to the description and analysis of hybrid systems. In Hybrid Systems, LNCS 736. Springer, Berlin Heidelberg New York:149–178
E.R. Olderog, A.P. Ravn, J.U. Skakkebæk (1996) Refining system requirements to program specifications. In Formal Methods in Real-Time Systems, Trends in Software-Engineering, chapter 5. Wiley
S. Owre, N. Shankar, J. Rushby (1993) Users guide for the pvs specification and verification system, language, and proof checker (beta release) (three volumes). Technical report, Computer Science Laboratory, SRI International, Menlo Park, CA
P. Øhrstrøm, P.F. Hasle (1995) Temporal Logic: From Ancient Ideas to Artificial Intelligence. Kluwer Academic
P.K. Pandya (1996) Some extensions to propositional mean value calculus: Expressiveness and decidability. In Computer Science Logic, CSL’95, LNCS 1092. Springer, Berlin Heidelberg New York:434–451
P.K. Pandya (1996) Weak chop inverses and liveness in duration calculus. In Formal Techniques in Real-Time and Fault-Tolerant Systems, LNCS 1135. Springer, Berlin Heidelberg New York:148–167
P.K. Pandya (2000) Specifying and deciding quantified discrete-time duration calculus formulae using DCVALID. Technical report TCS00-PKP-1, Tata Institute of Fundamental Research, India.
P.K. Pandya (1999) DCVALID 1.3: The user manual. Technical report TCS-99/1, Computer Science Group, TIFR, Bombay
P.K. Pandya, D.V. Hung (1998) Duration calculus with weakly monotonic time. In Formal Techniques in Real-Time and Fault-Tolerant Systems, LNCS 1486. Springer, Berlin Heidelberg New York:55–64
P.K. Pandya, Y.S. Ramakrishna, R.K. Shyamasundar (1995) A compositional semantics of Esterel in duration calculus. Technical report, Computer Science Group, TIFR, Bombay
L.C. Paulson (1994) Isabelle, A Generic Theorem Prover, LNCS 828. Springer Berlin Heidelberg New York
L.C. Paulson (1997) Proving properties of security protocols by induction. In Proceedings of the 10th IEEE Computer Security Foundations Workshop, Rockport, Mass. IEEE Press:70–83
J.L. Petersen, H. Rischel (1994) Formalizing requirements and design for a production cell system. In Symposium ADPM’ 94: Automatisation des Processus Mixtes: Les Systemes Dynamiques Hybrides. Belgian Institute of Automatic Control, IBRA:37–46
H. Pilegaard (2002) Modelling properties of security protocols. MA Thesis, Informatics and Mathematical Modelling, Technical University of Denmark
H. Pilegaard, M.R. Hansen, R. Sharp (2003) An approach to analyzing availability properties of security protocols. Nordic Journal of Computing 10:337–373
Z. Qiu, C. Zhou (1998) A combination of interval logic and linear temporal logic. In Programming Concepts and Methods. Chapman & Hall:444–461
A. Rabinovich (1998) Non-elementary lower bound for propositional duration calculus. Information Processing Letters: 7–11
A. Rabinovich (1998) On the decidability of continuous time specification formalism. Journal of Logic and Computation 8(5):669–678.
T.M. Rasmussen (1999) Signed interval logic. In Computer Science Logic, CSL’99, LNCS 1683. Springer Berlin Heidelberg New York:157–171
T.M. Rasmussen (2001) Automated proof support for interval logics. In LPAR 2001, LNAI 2250. Springer Berlin Heidelberg New York:317–326
T.M. Rasmussen (2001) Labelled natural deduction for interval logics. In Computer Science Logic, CSL’01, LNCS 2142. Springer Berlin Heidelberg New York:308–323
T.M. Rasmussen (2002) Interval Logic: Proof Theory and Theorem Proving. PhD Thesis, Informatics and Mathematical Modelling, Technical University of Denmark
A.P. Ravn, T.J. Eriksen, M. Holdgaard, H. Rischel (1998) Engineering of real-time systems with an experiment in hybrid control. In Embedded Systems, LNCS 1494. Springer Berlin Heidelberg New York:316–352
A.P. Ravn (1995) Design of Embedded Real-Time Computing Systems. Doctoral Dissertation, Department of Computer Science, Technical University of Denmark
A.P. Ravn, H. Rischel (1991) Requirements capture for embedded real-time systems. In Proceedings of IMACS-MCTS’91 Symposium on Modelling and Control of Technological Systems, Villeneuve d’Ascq, France, volume 2. IMACS:147–152
A.P. Ravn, H. Rischel, K.M. Hansen (1993) Specifying and verifying requirements of real-time systems. IEEE Transactions on Software Engineering 19(1):41–55
H. Rischel (1992) A duration calculus proof of fischer’s mutual exclusion protocol. ProCoS II, ESPRIT BRA 7071, Report No. DTH HR 4/1, Department of Computer Science, Technical University of Denmark
S. Roy, C. Zhou (1997) Notes on neighbourhood logic. UNU/IIST Report No. 97, International Institute for Software Technology, Macau
S. Satpathy, D.V. Hung, P.K. Pandya (1998) Some results on the decidability of duration calculus under synchronous interpretation. In Formal Techniques in Real-Time and Fault-Tolerant Systems, LNCS 1486. Springer, Berlin Heidelberg New York:186–197
M. Schenke (1994) Specification and transformation of reactive systems with time restrictions and concurrency. In Techniques in Real-Time and Fault-Tolerant Systems, LNCS 863. Springer, Berlin Heidelberg New York:605–620
M. Schenke (1995) Requirements to programs: A development methodology for real time systems, part 2. Technical report, Fachbereich Informatik, Universität Oldenburg, Germany
M. Schenke, E.R. Olderog (1995) Requirements to programs: A development methodology for real time systems, part 1. Technical report, Fachbereich Informatik, Universität Oldenburg, Germany
M. Schenke, A.P. Ravn (1996) Refinement from a control problem to programs. In Formal Methods for Industrial Applications, LNCS 1165. Springer Berlin Heidelberg New York:403–427
G. Schneider, Q. Xu (1998) Towards a formal semantics of verilog using duration calculus. In Formal Techniques in Real-Time and Fault-Tolerant Systems, LNCS 1486. Springer, Berlin Heidelberg New York:282–293
A. Schäfer (2004). A Calculus for Shapes in Time and Space. In Theoretical Aspects of Computing, ICTAC 2004, LNCS 3407. Springer Berlin Heidelberg New York:463–477
J.U. Skakkebæk (1994) Liveness and fairness in duration calculus. In CONCUR’94: Concurrency Theory, LNCS 836. Springer, Berlin Heidelberg New York: 283–298
J.U. Skakkebæk (1994) A Verification Assistant for a Real-Time Logic. PhD Thesis, Department of Computer Science, Technical University of Denmark
J.U. Skakkebæk, A.P. Ravn, H. Rischel, C. Zhou (1992) Specification of embedded, real-time systems. In Proceedings of 1992 Euromicro Workshop on Real-Time Systems. IEEE Computer Society Press
J.U. Skakkebæk, P. Sestoft (1994) Checking validity of duration calculus formulas. Technical report, ProCoS II, ESPRIT BRA 7071, report no. ID/DTH JUS 3/1, Department of Computer Science, Technical University of Denmark
J.U. Skakkebæk, N. Shankar (1994) Towards a duration calculus proof assistant in pvs. In Techniques in Real-Time and Fault-Tolerant Systems, LNCS 863. Springer, Berlin Heidelberg New York:660–679
E.V. Sørensen, A.P. Ravn, H. Rischel (1990) Control program for a gas burner: Part 1: Informal requirements, ProCoS case study 1. Technical Report ID/DTH EVS2
A. Tarski (1948) A decision method for elementary algebra and geometry. RAND Corporation, Santa Monica, California
Y. Venema (1990) Expressiveness and completeness of an interval tense logic. Notre Dame Journal of Formal Logic, 31(4):529–547
Y. Venema (1991) A modal logic for chopping intervals. Journal of Logic and Computation 1(4):453–476
L. Vigano (2000) Labelled non-classical logics. Kluwer Academic Punlishers
J. Wang, H. Weidong (1996) Formal specification of stability in hybrid control systems. In Hybrid Systems III, LNCS 1066. Springer, Berlin Heidelberg New York:294–303
B.H. Widjaja, W. He, Z. Chen, C. Zhou (1996) A cooperative design for hybrid control systems. In Proceedings of Logic and Software Engineering International Workshop in Honor of Chih-Sung Tang. World Scientific:127–150
Q. Xu, M. Swarup (1998) Compositional reasoning using assumption-commitment paradigm. In Compositionality-The Significant Difference, LNCS 1536. Springer Berlin Heidelberg New York:565–583
Q. Xu, H. Weidong (1996) Hierarchical design of a chemical concentration control system. In Hybrid Systems III: Verification and Control, LNCS 1066. Springer Berlin Heidelberg New York:270–281
Q. Xu, Z. Yang (1996) Derivation of control programs: a heating system. UNU/IIST Report No. 73, International Institute for Software Technology, Macau
X. Yu, J. Wang, C. Zhou, and P.K. Pandya (1994) Formal design of hybrid systems. In Techniques in Real-Time and Fault-Tolerant Systems, LNCS 863. Springer, Berlin Heidelberg New York:738–755
J. Zhao, D.V. Hung (1998) On checking real-time parallel systems for linear duration properties. In Formal Techniques in Real-Time and Fault-Tolerant Systems, LNCS 1486. Springer, Berlin Heidelberg New York:241–250
Y. Zheng, C. Zhou (1994) A formal proof of the deadline driven scheduler. In Techniques in Real-Time and Fault-Tolerant Systems, LNCS 863. Springer, Berlin Heidelberg New York:756–775
C. Zhou (1993) Duration Calculi: An overview. In Proceedings of Formal Methods in Programming and Their Applications, LNCS 735. Springer Berlin Heidelberg New York:256–266
C. Zhou, D.P. Guelev, N. Zhan (2000) A higher-order duration calculus. In Millennial Perspectives in Computer Science. Palgrave:407–416.
C. Zhou, M.R. Hansen (1996) Chopping a point. In BCS-FACS 7th Refinement Workshop. Electronic Workshops in Computing, Springer Berlin Heidelberg New York
C. Zhou, M.R. Hansen (1998) An adequate first order logic of intervals. In Compositionality: The Significant Difference, LNCS 1536. Springer Berlin Heidelberg New York:584–608
C. Zhou, M.R. Hansen, A.P. Ravn, H. Rischel (1991) Duration specifications for shared processors. In Symposium on Formal Techniques in Real-Time and Fault Tolerant Systems, LNCS 571. Springer Berlin Heidelberg New York:21–32
C. Zhou, M.R. Hansen (2004) Duration Calculus: A formal approach to realtime systems. Springer
C. Zhou, M.R. Hansen, P. Sestoft (1993) Decidability and undecidability results for duration calculus. In STACS’93, LNCS 665. Springer Berlin Heidelberg New York:58–68
C. Zhou, C.A.R. Hoare, A.P. Ravn (1991) A calculus of durations. Information Processing Letters 40(5):269–276
C. Zhou, D.V. Hung, X. Li (1995) A duration calculus with infinite intervals. In Fundamentals of Computation Theory, LNCS, Springer p. 16–41
X. Zhou, J. Wang, A.P. Ravn (1996) A formal description of hybrid systems. In Hybrid Systems III, LNCS 1066. Springer Berlin Heidelberg New York:511–530
C. Zhou, J. Zhang, L. Yang, X. Li (1994) Linear duration invariants. In Techniques in Real-Time and Fault-Tolerant Systems, LNCS 863. Springer, Berlin Heidelberg New York:86–109
C. Zhou, A.P. Ravn, M.R. Hansen (1993) An extended duration calculus for hybrid systems. In Hybrid Systems, LNCS 736. Springer, Berlin Heidelberg New York:36–59
C. Zhou, X. Li (1994) A mean value calculus of durations. In A Classical Mind: Essays in Honour of C.A.R. Hoare. Prentice Hall International:431–451
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this chapter
Cite this chapter
Hansen, M.R. (2008). Duration Calculus. In: Bjørner, D., Henson, M.C. (eds) Logics of Specification Languages. Monographs in Theoretical Computer Science. An EATCS Series. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-74107-7_6
Download citation
DOI: https://doi.org/10.1007/978-3-540-74107-7_6
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-74106-0
Online ISBN: 978-3-540-74107-7
eBook Packages: Computer ScienceComputer Science (R0)