Abstract
We propose a model independent procedure for verifying properties of
discrete event systems. The dynamics of such systems can be very
complex, making them hard to analyze, so we resort to methods based on
Monte Carlo simulation and statistical hypothesis testing. The
verification is probabilistic in two senses. First, the properties,
expressed as CSL formulas, can be probabilistic. Second, the result
of the verification is probabilistic, and the probability of error is
bounded by two parameters passed to the verification procedure. The
verification of properties can be carried out in an anytime manner by
starting off with loose error bounds, and gradually tightening these
bounds.
Full paper: PDF, PS (13 pages, 16 references)
© Springer-Verlag Berlin Heidelberg 2002
Presentation: PDF (43 slides)
Citings
Rajeev Alur and Mikhail Bernadsky. 2006. Bounded model checking for GSMP models of stochastic real-time systems. In Proceedings of the 9th International Workshop on Hybrid Systems: Computation and Control, 19–33. Springer.
Christel Baier, Boudewijn R. Haverkort, Holger Hermanns, and Joost-Pieter Katoen. 2005. Model checking meets performance evaluation. ACM SIGMETRICS Performance Evaluation Review 32(4):10–15.
Pedro R. D'Argenio and Joost-Pieter Katoen. 2005. A theory of stochastic systems. Part I: Stochastic automata. Information and Computation 203(1):1–38.
Rocco De Nicola, Diego Latella, and Mieke Massink. 2005. Formal modeling and quantitative analysis of KLAIM-based mobile systems. In Proceedings of the 2005 ACM Symposium on Applied Computing, 428–435. ACM Press.
Radu Grosu and Scott A. Smolka. 2005. Monte Carlo model checking. In Proceedings of the 11th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, 271–286. Springer.
Holger Hermanns, David N. Jansen, and Yaroslav S. Usenko. 2005. From StoCharts to MoDeST: A comparative reliability analysis of train radio communications. In Proceedings of the 5th International Workshop on Software and Performance, 13–23. ACM Press.
David N. Jansen and Holger Hermanns. 2005. QoS modelling and analysis with UML-statecharts: The StoCharts approach. ACM SIGMETRICS Performance Evaluation Review 32(4):28–33.
Iman Poernomo, Jane Jayaputera, and Heinz Schmidt. 2005. Timed probabilistic constraints over the distributed management taskforce common information model. In Proceedings of the Ninth IEEE International EDOC Enterprise Computing Conference, 261–272. IEEE Computer Society.
Usa Sammapun, Insup Lee, and Oleg Sokolsky. 2005. RT-MaC: Runtime monitoring and checking of quantitative and probabilistic properties. In Proceedings of the 11th IEEE International Conference on Embedded and Real-Time Computing Systems and Applications, 147–153. IEEE Computer Society.
Koushik Sen, Mahesh Viswanathan, and Gul Agha. 2005. VeStA: A Statistical model-checker and analyzer for probabilistic systems. In Proceedings of the Second International Conference on the Quantitative Evaluation of Systems, 251–252. IEEE Computer Society.
Koushik Sen, Mahesh Viswanathan, and Gul Agha. 2005. On statistical model checking of stochastic systems. In Proceedings of the 17th International Conference on Computer Aided Verification, 266–280. Springer.
Thomas Hérault, Richard Lassaigne, Frédéric Magniette, and Sylvian Peyronnet. 2004. Approximate probabilistic model checking. In Proceedings of the 5th International Conference on Verification, Model Checking, and Abstract Interpretation, 73–84. Springer.
David N. Jansen and Holger Hermanns. 2004. Dependability checking with StoCharts: In train radio reliable enough for trains?. In Proceedings of the First International Conference on the Quantitative Evaluation of Systems, 250–259. IEEE Computer Society.
Mieke Massink, Joost-Pieter Katoen, and Diego Latella. 2004. Model checking dependability attributes of wireless group communication. In Proceedings of the 2004 International Conference on Dependable Systems and Networks, 711–720. IEEE Computer Society.
Koushik Sen, Mahesh Viswanathan, and Gul Agha. 2004. Statistical model checking of black-box probabilistic systems. In Proceedings of the 16th International Conference on Computer Aided Verification, 202–215. Springer.
Jeremy Sproston. 2004. Model checking for probabilistic timed systems. In Validation of Stochastic Systems: A Guide to Current Research, 189–229. Springer.
Christel Baier, Boudewijn R. Haverkort, Holger Hermanns, and Joost-Pieter Katoen. 2003. Model-checking algorithms for continuous-time Markov chains. IEEE Transactions on Software Engineering 29(6):524–541.
Jeremy T. Bradley, Nicholas J. Dingle, Peter G. Harrison, and William J. Knottenbelt. 2003. Performance queries on semi-Markov stochastic Petri nets with an extended continuous stochastic logic. In Proceedings of the 10th International Workshop on Petri Nets and Performance Models, 62–71. IEEE Computer Society.
David N. Jansen, Holger Hermanns, and Joost-Pieter Katoen. 2003. A QoS-oriented extension of UML statecharts. In Proceedings of the 6th International Conference on the Unified Modeling Language, 76–91. Springer.
Nirman Kumar, Koushik Sen, José Meseguer, and Gul Agha. 2003. A rewriting based model for probabilistic distributed object systems. In Proceedings of the 6th IFIP WG 6.1 International Conference on Formal Methods for Open Object-Based Distributed Systems, 32–46. Springer.
Marta Kwiatkowska. 2003. Model checking for probability and time: From theory to practice. In Proceedings of the 18th Annual IEEE Symposium on Logic in Computer Science, 351–360. IEEE Computer Society.
N. Markey and P. Schonoebelen. 2003. Model checking a path (preliminary report). In Proceedings of the 14th International Conference on Concurrency Theory, 251–265. Springer.
Håkan L. S. Younes | [ Home > Publications ] | |
Last modified: Fri Apr 28 11:11:19 EDT 2006 |