A Probabilistic Duration Calculus

  • Z. Liu
  • A. P. Ravn
  • E. V. Sørensen
  • C. Zhou
Part of the Dependable Computing and Fault-Tolerant Systems book series (DEPENDABLECOMP, volume 7)

Abstract

This paper presents a calculus that enables a designer of an embedded, real-time system to reason about and calculate whether a given requirement will hold with a sufficient high probability for given failure probabilities for components used in the design of the system. The main idea is to specify requirements and design in Duration Calculus, a real-time, interval logic, to define satisfaction probabilities for formulas in this calculus, and establish a calculus with rules that support calculation of the probability for a composite formula from probabilities of its constituents. This ensures that reasoning about probabilities is consistent with requirements and design decisions. We thus avoid introducing separate models for requirements and reliability analysis. The system model is a finite automaton with fixed transition probabilities. This defines discrete Markov processes as basis for the calculus.

Key Words

duration calculus real-time systems probabilistic automata satisfaction probability 

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. [1]
    E. S0rensen, J. Nordahl, and N. Hansen, “From CSP models to Markov models: a case study,” Tech. Rep. ProCos, Institute of Computer Science, Technical University of Denmark, DK-2800 Lyngby, Denmark, 1991. Accepted by IEEE Transactions on Software Engineering.Google Scholar
  2. [2]
    C. Zhou, C. Hoare, and A. Ravn, “A calculus of durations,” Information Processing Letters, vol. 40, no. 5, pp. 269–276, 1992.MathSciNetGoogle Scholar
  3. [3]
    K. Hansen, A. Ravn, and H. Rischel, “Specifying and verifying requirements of real-time systems,” ACM SIGSOFT ’91 Conference on Software for Critical Systems, December 1991.Google Scholar
  4. [4]
    A. Ravn and H. Rischel, “Requirements capture for embedded real-time systems,” IMACS-IFACSymposium MCTS, Lille, France, pp. vol. 2, pp. 147–152, 1991.Google Scholar
  5. [5]
    J. Skakkebaek, A. Ravn, H. Rischel, and C. Zhou, “Specification of embedded, real-time systems,” Proc. of EuroMicro Workshop on Real-Time Systems, (Athens, Greece), pp. 116–121, IEEE Computer Society Press, Los Alamos, Cahfornia, 3–5, June 1992.Google Scholar
  6. [6]
    P. M. Melhar-Smith and R. L. Schwartz, “Formal specification and mechanical verification of SIFT: A fault tolerant flight control system,” IEEE Trans, on Computers, vol. 31, no. 7, 1982.Google Scholar
  7. 7]
    H. Hansson and B. Jonsson, “A framework for reasoning about time and rehability,” Proc. of 10th IEEE Real-Time System Symposium, Sta. Monica, Ca., 1989.Google Scholar
  8. [8]
    K. Larsen and A. Skou, “Bisimulation through probabilistic testing,” in Proc. of 16th ACM Symposium on Principles of Programming Languages, 1989.Google Scholar
  9. [9]
    E. Clarke, E. Emerson, and A. Sistla, “Automatic verification of finite-state concurrent systems using temporal logic specification: A practical approach,” in Proc. of 10th ACM Symp. on Principles of Programming Languages, pp. 117–126, 1983.Google Scholar
  10. [10]
    M. R. Hansen and C. Zhou, “Semantics and completeness of duration calculus,” Lecture Notes in Computer Science 600 (W.-P. d. R. J.W. de Bakker and G. Rozenberg, eds.), pp. 209–226, Springer-Verlag, 1991.Google Scholar
  11. [11]
    W. Feller, An Introduction to Probability Theory and Its Applications, vol. 2. John Wiley & Sons, Inc. New York, London, 2nd ed., 1966.MATHGoogle Scholar
  12. 12]
    G. E. Hughes and M. J. Cresswell, A Companion to Modal Logic. London: Methuen and Co., 1984.MATHGoogle Scholar
  13. [13]
    Z. Liu, Fault-Tolerant Programming by Transformations. PhD thesis. Department of Computer Science, University of Warwick, Coventry CV4 7AL, UK, 1991.Google Scholar
  14. [14]
    Z. Liu and M. Joseph, “Transformation of programs for fault-tolerance,” Formal Aspects of Computing, vol. 4, no. 5, pp. 442–469, 1992.MATHCrossRefGoogle Scholar
  15. [15]
    J. Nordahl, Specification and Design of Dependable Communicating Systems. PhD thesis. Department of Computer Science, Technical University of Denmark, DK-2800 Lyngby, Denmark, 1992.Google Scholar

Copyright information

© Springer-Verlag/Wien 1993

Authors and Affiliations

  • Z. Liu
    • 1
  • A. P. Ravn
    • 2
  • E. V. Sørensen
    • 2
  • C. Zhou
    • 3
    • 4
  1. 1.Department of Computer ScienceUniversity of WarwickCoventryEngland, UK
  2. 2.Department of Computer ScienceTechnical University of DenmarkLyngbyDenmark
  3. 3.International Institute for Software TechnologyUnited Nations UniversityMacauChina
  4. 4.Software InstituteAcademia SinicaBeijingP.R. China

Personalised recommendations