Abstract
Many reactive systems are actually Stochastic Processes. Automatic analysis of such systems is usually very difficult thus typically one simplifies the analysis task by using simulation or by working on a simplified model (e.g. a Markov Chain).
We present a Finite Horizon Probabilistic Model Checking approachwhich essentially can handle the same class of stochastic processes of a typical simulator. This yields easy modeling of the system to be analysed together with formal verification capabilities. Our approach is based on a suitable disk based extension of the Murφ verifier.
Moreover we present experimental results showing effectiveness of our approach.
This research has been partially supported by MURST projects: MEFISTO and SAHARA
This is a preview of subscription content, log in via an institution to check access.
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
Apt, K.R., Olderog, E.-R.: Verification of Sequential and Concurrent Programs. Text and Monographs in Computer Science. Springer, Heidelberg (1991)
Baier, C., Clarke, E.M., Hartonas-Garmhausen, V., Kwiatkowska, M., Ryan, M.: Symbolic model checking for probabilistic processes. Automata, Languages and Programming, 430–440 (1997)
Behrends, E.: Introduction to Markov Chains. Vieweg (2000)
Bianco, A., de Alfaro, L.: Model checking of probabilistic and nondeterministic systems. In: Thiagarajan, P.S. (ed.) FSTTCS 1995. LNCS, vol. 1026, pp. 499–513. Springer, Heidelberg (1995)
Burch, J.R., Clarke, E.M., McMillan, K.L., Dill, D.L., Hwang, L.J.: Symbolic model checking: 1020 states and beyond. Information and Computation 98 (1992)
Courcoubetis, C., Yannakakis, M.: Verifying temporal properties of finite-state probabilistic programs. In: Proc. of FOCS 1988, pp. 338–345. IEEE CS Press, Los Alamitos (1988)
Courcoubetis, C., Yannakakis, M.: The complexity of probabilistic verification. J. ACM 42(4), 857–907 (1995)
de Alfaro, L.: Formal verification of performance and reliability of real-time systems. Technical report, Stanford University (1996)
Dill, D.L., Drexler, A.J., Hu, A.J., Yang, C.H.: Protocol verification as a hardware design aid. In: IEEE International Conference on Computer Design: VLSI in Computers and Processors, pp. 522–525 (1992)
Hermanns, H., Infante Lopez, G.G., Katoen, J.: Beyond memoryless distribution: Model checking semi-markov chains. In: de Luca, L., Gilmore, S. (eds.) PROBMIV 2001, PAPM-PROBMIV 2001, and PAPM 2001. LNCS, vol. 2165, pp. 57–70. Springer, Heidelberg (2001)
Hansson, H.: Time and Probability in Formal Design of Distributed Systems. Elsevier, Amsterdam (1994)
Hansson, H., Jonsson, B.: A logic for reasoning about time and probability. Formal Aspects of Computing 6, 512–535 (1994)
Holzmann, G.J.: Design and Validation of Computer Protocols. Prentice Hall, New Jersey (1991)
Holzmann, G.J.: The spin model checker. IEEE Trans. on Software Engineering 23(5), 279–295 (1997)
Kwiatkowska, M., Norman, G., Parker, D.: PRISM: Probabilistic symbolic model checker. In: Kemper, P. (ed.) Proc. Tools Session of Aachen 2001 International Multiconference on Measurement, Modelling and Evaluation of Computer-Communication Systems, September 2001, pp. 7–12 (2001); Available as Technical Report 760/2001, University of Dortmund.
Kwiatkowska, M., Norman, G., Parker, D.: Probabilistic symbolic model checking with prism: A hybrid approach. In: Katoen, J.-P., Stevens, P. (eds.) TACAS 2002. LNCS, vol. 2280, p. 52. Springer, Heidelberg (2002)
Larsen, K., Skou, A.: Bisimulation through probabilistic testing. Information and Computation 94, 1–28 (1991)
Nelson, B.L.: Stochastic Modeling: Analysis And Simulation. Dover Publications, New York (1995)
Papoulis, A.: Probability, Random Variables and Stochastic Processes. McGraw-Hill Series in System Sciences (1965)
Della Penna, G., Intrigila, B., Melatti, I., Minichino, M., Ciancamerla, E., Parisse, A., Tronci, E., Zilli, M.V.: Automatic verification of a turbogas control system with the murphi verifier. In: Maler, O., Pnueli, A. (eds.) HSCC 2003. LNCS, vol. 2623, pp. 141–155. Springer, Heidelberg (2003)
Della Penna, G., Intrigila, B., Melatti, I., Tronci, E., Zilli, M.V.: Finite horizon analysis of markov chains with the murphi verifier (2003) (submitted for publication)
Pnueli, A., Zuck, L.: Probabilistic verification. Information and Computation 103, 1–29 (1993)
Segala, R., Lynch, N.: Probabilistic simulations for probabilistic processes. In: Jonsson, B., Parrow, J. (eds.) CONCUR 1994. LNCS, vol. 836, pp. 381–496. Springer, Heidelberg (1994)
Vardi, M.: Automatic verification of probabilistic concurrent finite-state programs. In: Proc. of FOCS 1985, pp. 327–338. IEEE CS Press, Los Alamitos (1985)
de Alfaro, L., Henzinger, T.A., Majumdar, R.: Discounting the Future in Systems Theory. In: Baeten, J.C.M., Lenstra, J.K., Parrow, J., Woeginger, G.J. (eds.) ICALP 2003. LNCS, vol. 2719, pp. 1022–1037. Springer, Heidelberg (2003)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2003 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Della Penna, G., Intrigila, B., Melatti, I., Tronci, E., Zilli, M.V. (2003). Finite Horizon Analysis of Stochastic Systems with the Murφ Verifier. In: Blundo, C., Laneve, C. (eds) Theoretical Computer Science. ICTCS 2003. Lecture Notes in Computer Science, vol 2841. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-45208-9_6
Download citation
DOI: https://doi.org/10.1007/978-3-540-45208-9_6
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-20216-5
Online ISBN: 978-3-540-45208-9
eBook Packages: Springer Book Archive