Abstract
Probabilistic correctness is an important aspect of reliable systems. A soft real-time system, for instance, may be designed to tolerate some degree of deadline misses under a threshold. Since probabilistic systems may behave differently from their probabilistic models depending on their current environments, checking the systems at runtime can provide another level of assurance for their probabilistic correctness. This paper presents a statistical runtime verification for probabilistic properties using statistical analysis. However, while this statistical analysis collects a number of execution paths as samples to check probabilistic properties within some certain error bounds, runtime verification can only produce one single sample. This paper provides a technique to produce such a number of samples and applies this methodology to check probabilistic properties in wireless sensor network applications.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Barringer, H., Goldberg, A., Havelund, K., Sen, K.: Rule-based runtime verification. In: Proceedings of 5th International Conference on Verification, Model Checking and Abstract Interpretation, Vanice, Italy, pp. 44–57 (2004)
Culler, D.E., Hill, J., Buonadonna, P., Szewczyk, R., Woo, A.: A network-centric approach to embedded software for tiny devices. In: Henzinger, T.A., Kirsch, C.M. (eds.) EMSOFT 2001. LNCS, vol. 2211, Springer, Heidelberg (2001)
Devore, J.L.: Probability and Statistics for Engineering and the Sciences. Duxbury Thomson Learning (2000)
Drusinsky, D.: Monitoring temporal rules combined with Time Series. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, Springer, Heidelberg (2003)
Finkbeiner, B., Sankaranarayanan, S., Sipma, H.B.: Collecting statistics about runtime executions. Formal Methods in System Design 27(3), 253–274 (2005)
Gay, D., Levis, P., von Behren, R., Welsh, M., Brewer, E., Culler, D.: The nesC language: A holistic approach to networked embedded systems. In: Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (2003)
Havelund, K., Roşu, G.: Java PathExplorer – A runtime verification tool. In: Proceedings of the 6th International Symposium on Artificial Intelligence, Robotics and Automation in Space (2001)
Jayaputera, J., Poernomo, I., Schmidt, H.: Runtime verification of timing and probabilistic properties using WMI and .NET. In: Proceedings of the 30th EUROMICRO Conference (2004)
Kim, M., Kannan, S., Lee, I., Sokolsky, O., Viswanathan, M.: Java-MaC: a runtime assurance approach for Java programs. Formal Methods in Systems Design 24(2), 129–155 (2004)
Kristoffersen, K.J., Pedersen, C., Anderson, H.R.: Runtime verification of Timed LTL using disjunctive normalized equation systems. In: Proceedings of the 3rd International Workshop on Runtime Verification (2003)
Manna, Z., Pnueli, A.: The Temporal Logic of Reactive and Concurrent Systems. Springer, Heidelberg (1992)
Sammapun, U., Lee, I., Sokolsky, O.: RT-MaC: Runtime monitoring and checking of quantitative and probabilistic properties. In: Proceedings of the 11th IEEE International Conference of Embedded and Real-Time Computing Systems and Applications (2005)
Stolz, V., Bodden, E.: Temporal assertions using AspectJ. In: Proceedings of the 5th International Workshop on Runtime Verification (July 2005)
Titzer, B.L.: Avrora: The AVR simulation and analysis framework. Master’s thesis, University of California, Los Angeles, June (2004)
Wald, A.: Sequential Analysis. In: Dover Phoenix Editions (2004)
Younes, H.L.S., Kwiatkowska, M., Norman, G., Parker, D.: Numerical vs. statistical probabilistic model checking: An empirical study. In: Proceedings of the 10th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (2004)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2007 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Sammapun, U., Lee, I., Sokolsky, O., Regehr, J. (2007). Statistical Runtime Checking of Probabilistic Properties. In: Sokolsky, O., Taşıran, S. (eds) Runtime Verification. RV 2007. Lecture Notes in Computer Science, vol 4839. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-77395-5_14
Download citation
DOI: https://doi.org/10.1007/978-3-540-77395-5_14
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-77394-8
Online ISBN: 978-3-540-77395-5
eBook Packages: Computer ScienceComputer Science (R0)