This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
From CSP Models to Markov Models
June 1993 (vol. 19 no. 6)
pp. 554-570

It is shown how a probabilistic dependability model of a safety-critical system can be derived from a trace-based functional model of the system. The functional model is a communicating sequential process (CSP) that includes command, failure, and repair events. The dependability model is a time homogeneous Markov process with transitions determined by these events. The method applies to deterministic systems that can be described in terms of a finite number of states and in which all event occurrences are stochastic with exponential time distribution. The derivation is carried out in two steps. An algorithmic determination is made of a finite automaton from the specification of the CSP process. The automaton is transformed into a Markov process. The Markov model for this system is used to determine the waiting time to terminal failure. The theory is applied to a larger and more realistic example: a gas burner system operating in the on-off mode. For this system, the waiting time to terminal failure is calculated, and the number of failures per year in a large population of identical, independently operated systems is estimated.

[1] C.A.R. Hoare,Communicating Sequential Processes, Prentice Hall, Englewood, N.J., 1985.
[2] K. S. Trivedi,Probability and Statistics with Reliability, Queueing and Computer Science Applications. Englewood Cliffs, NJ: Prentice-Hall, 1982.
[3] D. R. Cox and H, D. Miller,The Theory of Stochastic Processes. London: Chapmann and Hall, 1965 (reprinted 1968, 1970, 1972, 1980, 1984, and 1990).
[4] P. M. Melliar-Smith and R. L. Schwarts, "Formal specification and mechanical verification of SIFT: A fault tolerant flight control system,"IEEE Trans. Comput., vol. C-31, July 1982.
[5] H. Hansson and B. Jonsson, "A framework for reasoning about time and reliability," inProc. 10th IEEE Real-Time Symp., Santa Monica, CA, 1989.
[6] E. Emerson and E. Clarke, "Using branching time temporal logic to synthezise synchronization skeletons,"Sci. Comput. Programming, vol. 2, no. 3, 1982.
[7] Z. Liu, A. P. Ravn, E. V. Sørensen, and C. C. Zhou, "A probabilistic duration calculus," presented at the 2nd Int. Workshop Responsive Comput. Syst., Japan, 1992.
[8] C. C. Zhou, C. A. R. Hoare, and A. P. Ravn, "A calculus of durations,"Inform. Processing Lett., vol. 40, no. 5, 1992.
[9] C. C. Zhou and M. R. Hansen, "Semantics and completeness of duration calculus," ProCoS Working Paper, accepted for the REX'92 Symp.
[10] N. H. Hansen and E. V. Sørensen, "On the risk prediction for repairable safety critical systems, A theoretical foundation," ProCoS Rep. ID/DTH, Nov. 30, 1990.
[11] J. C. Laprie, "Dependability: Basic concepts and associated terminology," PDCS Rep., LAAS-CNRS, Toulouse, France, May 1990. Key document in IFIP WG 10.4, "Dependable computing and fault tolerance."
[12] B.W. Johnson, "Evaluation techniques," ch. 4 inDesign and Analysis of Fault Tolerant Digital Systems. Reading, MA: Addison-Wesley, 1989.
[13] H. Cramér and M. R. Leadbetter,Stationary and Related Stochastic Processes. New York: Wiley, 1967.
[14] J. H. Wilkinson,The Algebraic Eigenvalue Problem. London, England: Oxford University Press, 1965.
[15] J. Nordahl, "Specification and design of dependable communicating systems," Ph.D. dissertation, Depo Comput. Sci., DTH, 1992.
[16] E. V. Sørensen, A. P. Ravn, and H. Rischel, "Control program for a gas burner: Part 1: Informal requirements," ProCoS Case Study 1, ProCoS Rep., Mar. 1990.

Index Terms:
probabilistic dependability model; safety-critical system; trace-based functional model; communicating sequential process; time homogeneous Markov process; deterministic systems; event occurrences; stochastic; exponential time distribution; finite automaton; specification; waiting time; terminal failure; gas burner system; communicating sequential processes; fault tolerant computing; finite automata; Markov processes
Citation:
E.V. Sorensen, J. Nordahl, M.H. Hansen, "From CSP Models to Markov Models," IEEE Transactions on Software Engineering, vol. 19, no. 6, pp. 554-570, June 1993, doi:10.1109/32.232021
Usage of this product signifies your acceptance of the Terms of Use.