A Probabilistic Duration Calculus
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 Wordsduration calculus real-time systems probabilistic automata satisfaction probability
Unable to display preview. Download preview PDF.
- 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
- 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
- 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
- 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
- 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]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
- K. Larsen and A. Skou, “Bisimulation through probabilistic testing,” in Proc. of 16th ACM Symposium on Principles of Programming Languages, 1989.Google Scholar
- 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
- 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
- Z. Liu, Fault-Tolerant Programming by Transformations. PhD thesis. Department of Computer Science, University of Warwick, Coventry CV4 7AL, UK, 1991.Google Scholar
- 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