Exponentially timed SADF: Compositional semantics, reductions, and analysis

This paper presents a rigorous compositional semantics for SADF (Scenario-Aware Data Flow), an extension of SDF for scenario-based embedded system design which has its roots in digital signal processing. We show that Markov automata (MA), a novel combination of probabilistic automata and continuous-time Markov decision processes, provides a natural semantics when all execution times are exponential. The semantics is fully compositional, i.e., each SADF agent is modeled by a single automaton which are all put in parallel. We show how stochastic model checking can be used to analyse the MA, yielding measures such as expected time, long-run objectives, throughput, and timed reachability. Using aggressive reduction techniques for Markov automata that are akin to partial-order reduction, scalability of analysis is achieved, and all non-determinism can be eliminated.