Probabilistic Analysis of Real-Time Systems
This page is under construction.
Variations in behavior of a system can often be characterized by means of probabilistic information in the specification. Probabilistic analysis methods then provide quantitative information of about system's behavior.
We adopt the view that variations in a system's behavior usually come from failures of certain resources, such as processors, communication channels, etc.
Therefore, a natural way to express these variations is provided by a
probabilistic extension of (ACSR), which already has facilities to express resource usage. Probabilistic ACSR (PACSR) associates a probability of failure with each resource in the specification. The resulting formalism is a conservative extension of ACSR that provides a natural way to reason about resource failures and recoveries and other aspects of probabilistic behavior.
A suite of analysis methods has been developed for Labeled Concurrent Markov Chains, a model that covers PACSR specifications and many other probabilistic specification formalisms.
Publications
- Specifying Failures and Recoveries in PACSR, A. Philippou, O. Sokolsky, I. Lee, R. Cleaveland, and S.A. Smolka, Proceedings of Workshop on Probabilistic Methods in Verification, Jun 1998.
Abstract
- Full Postscript File
- Probabilistic Resource Failure in Real-Time Process Algebra, A. Philippou, R. Cleaveland, I. Lee, S.A. Smolka, and O. Sokolsky, To appear at CONCUR '98
Abstract
- Full Postscript File