Formally Verifying Decompositions of Stochastic Specifications

According to the principles of compositional verification, verifying that lower-level components satisfy their specification will ensure that the whole system satisfies its top-level specification. The key step is to ensure that the lower-level specifications constitute a correct decomposition of the top-level specification. In a non-stochastic context, such decomposition can be analyzed using techniques of theorem proving. In industrial applications, especially for safety-critical systems, specifications are often of stochastic nature, for example giving a bound on the probability that system failure will occur before a given time. A decomposition of such a specification requires techniques beyond traditional theorem proving. The first contribution of the paper is a theoretical framework that allows the representation of, and reasoning about, stochastic and timed behavior of systems as well as specifications for such behaviors. The framework is based on traces that describe the continuoustime evolution of a system, and specifications are formulated using timed automata combined with probabilistic acceptance conditions. The second contribution is a novel approach to verifying decomposition of such specifications by reducing the problem to checking emptiness of the solution space for a system of linear inequalities.