Abstract
Model checking can tell us whether a system is correct; probabilistic model checking can also tell us whether a system is timely and reliable. Moreover, probabilistic model checking allows one to verify properties that may not be true with probability one, but may still hold with an acceptable probability. The challenge in developing a probabilistic model checker able to handle realistic systems is the construction of the state space and the necessity to solve huge systems of linear equations. To address this problem, we have developed ProbVerus, a tool for the formal verification of probabilistic real-time systems. ProbVerus is an implementation of probabilistic computation tree logic (PCTL) model checking using symbolic techniques. We present ProbVerus, demonstrate its use with a simple manufacturing example, and report the current status of the tool. With ProbVerus, we have been able to analyze, within minutes, the safety logic of a railway interlocking controller with 1027 states.
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
R. Alur, C. Courcoubetis, D. Dill. Model Checking for Probabilistic Real-time Systems. Automata, Languages, and Programming 18th International Colloquium Proceedings; Madrid, Spain; 8–12 July 1991.
A. Aziz, V. Singhal, F. Balarin, R. K. Brayton, A.L. Sangiovanni-Vincentelli. It usually works: the temporal logic of stochastic systems. In Proceedings of CAV’95.
R. E. Bryant. Graph-based algorithms for boolean function manipulation. IEEE Transactions on Computers, C-35(8), 1986.
S. Campos, E. Clarke, W. Marrero, M. Minea and H. Hiraishi, Computing quantitative characteristics of finite-state real-time systems. In IEEE Real-Time Systems Symposium, 1994.
S. Campos and E. Clarke, Real-time symbolic model checking for discrete time models. In AMAST Series in Computing: Theories and Experiences for Real-Time System Development. T. Rus, C. Rattray, editors. World Scientific Publishing Company, 1995.
S. V. Campos. A Quantitative Approach to the Formal Verification of Real-Time Systems. Ph.D. Thesis, School of Computer Science, Carnegie Mellon University, 1996.
E. M. Clarke, E. A. Emerson. Synthesis of Synchronization Skeletons for Branching Time Temporal Logic. Logic of Programs: Workshop, Yorktown Heights, NY, May 1981, volume 131 of Lecture Notes in Computer Science. Springer Verlag, 1981.
E. M. Clarke, M. Fujita, P.C. McGeer, K. McMillan, J. C.-Y. Yang, X. Zhao. Multi-Terminal Binary Decision Diagrams: An Efficient Data Structure for Matrix Representation. IWLS’ 93: International Workshop on Logic Synthesis. Tahoe City, May 1993.
C. Courcoubetis, M. Yannakakis. The Complexity of Probabilistic Verification. Journal of the Association for Computing Machinery, Vol. 42, No. 4, July 1995.
G. Hachtel, E. Macii, A. Pardo, F. Somenzi. Markovian Analysis of Large Finite State Machines. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, Vol. 15. No. 12, December 1996.
H. Hansson and B. Jonsson. A Framework for Reasoning about Time and Reliability. In Proceedings of 10th IEEE Real Time System Symposium, pp. 102–111, 1989.
H. Hansson. Time and Probability in Formal Design of Distributed Systems. Elsevier, 1994.
S. Hart and M. Sharir. Probabilistic Temporal Logics for Finite and Bounded Models. In Proceedings of the ACM Symposium on the Theory of Computing, pp. 1–13, 1984.
V. Hartonas-Garmhausen, S. Campos, A. Cimatti, E. Clarke, F. Giunchiglia. Verification of a Safety-Critical Railway Interlocking System with Real-Time Constraints. In Proceedings of FTCS-28 The Twenty-Eighth Annual International Symposium on Fault-Tolerant Computing, pages 458–463, June, 1998.
V. Hartonas-Garmhausen. Probabilistic Symbolic Model Checking with Engineering Models and Applications. Ph.D. Thesis. Carnegie Institute of Technology, Carnegie Mellon University, 1998.
D. Lehmann and S. Shelah. Reasoning with time and chance. Information and Control 53, pp. 165–198, 1982.
M. Vardi. Automatic verification of probabilistic concurrent finite-state programs. In Proceedings of the 26th IEEE Symposium on Foundations of Computer Science. IEEE, New York, pp. 327–338, 1985.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1999 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Hartonas-Garmhausen, V., Campos, S., Clarke, E. (1999). ProbVerus: Probabilistic Symbolic Model Checking. In: Katoen, JP. (eds) Formal Methods for Real-Time and Probabilistic Systems. ARTS 1999. Lecture Notes in Computer Science, vol 1601. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-48778-6_6
Download citation
DOI: https://doi.org/10.1007/3-540-48778-6_6
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-66010-1
Online ISBN: 978-3-540-48778-4
eBook Packages: Springer Book Archive