Probabilistic Model Checking for Uncertain Scenario-Aware Data Flow

The Scenario-Aware Dataflow (SADF) model is based on concurrent actors that interact via channels. It combines streaming data and control to capture scenarios while incorporating hard and soft real-time aspects. To model data-flow computations that are subject to uncertainty, SADF models are equipped with random primitives. We propose to use probabilistic model checking to analyze uncertain SADF models. We show how measures such as expected time, long-run objectives like throughput, as well as timed reachability-can a given system configuration be reached within a deadline with high probability?-can be automatically determined. The crux of our method is a compositional semantics of SADF with exponential agent execution times combined with automated abstraction techniques akin to partial-order reduction. We present the semantics in detail and show how it accommodates the incorporation of execution platforms, enabling the analysis of energy consumption. The feasibility of our approach is illustrated by analyzing several quantitative measures of an MPEG-4 decoder and an industrial face recognition application.