Model checking of finite-state machine-based scenario-aware dataflow using timed automata

Dataflow formalisms are widely used for modeling and analyzing streaming applications. An important distinction is between static and dynamic formalisms, the latter allowing for the workload to change on-the-fly. The recently introduced finite-state machine based scenario aware dataflow (FSM-SADF) is a dynamic dataflow formalism that increases the expressiveness of the static synchronous dataflow (SDF) formalism, by allowing finite-state control, while to a large extent retaining its design-time analyzability. This paper reports on the translation of the FSM-SADF formalism to UPPAAL timed automata that enables a more general verification than currently supported by existing tools. We base our translation on a compositional approach where the input FSM-SADF model is represented as a parallel composition of its integral components modeled as automata. Thereafter, we show how to model check quantitative and qualitative properties both supported and not supported by the existing tools. We demonstrate our approach on a realistic case study from the multimedia domain.