Model Checking of Scenario-Aware Dataflow

Organisation:	Embedded Systems Institute, Eindhoven (THE NETHERLANDS) RWTH Aachen (GERMANY)
Method:	SADF
Tools used:	CADP (Construction and Analysis of Distributed Processes) SDF3
Domain:	Embedded Systems.
Period:	2012
Size:	n/a.
Description:	Model-based design of distributed (multi-core) streaming applications like MPEG-4 and MP3 decoding often use dataflow-based analysis and synthesis techniques. Many such approaches rely on the formalism of (Homogeneous) Synchronous Dataflow ((H)SDF), also known as (Weighted) Marked Graphs in Petri Net theory. A wide range of design-time analysis techniques have been developed for SDF, covering both functional properties such as absence of deadlock and the key performance properties of throughput, latency, and buffer occupancy. However, SDF only handles fixed behavioural patterns, therefore not capturing the dynamism of certain applications (e.g., decoding different types of video frames in MPEG-4), which imply large variations in resource usage. Neglecting such resource usage variations during design-time analysis may lead to substantially overdimensioning. The formalism of Scenario-Aware Dataflow (SADF) has recently been introduced as an alternative that does allow modelling dynamic behavior, while various design-time analysis techniques are available and efficient implementations can be created. SADF is equipped with state-of-the-art analysis techniques, such as those supported by the SDF3 tool suite (worst-case performance analysis, model checking techniques for computing throughput, expected response time, and maximum buffer occupancy, etc.). The model checking based analysis does however not use existing (quantitative) model checkers, thereby lacking flexible support for evaluating user-defined properties (i.e., properties other than certain predefined ones). This study reports on an investigation to apply the CADP toolbox for quantitative analysis and qualitative model checking of SADF. This enables the usage of powerful (compositional) state-space reduction techniques as well as checking a large range of functional properties expressed in the temporal logic XTL. To enable using CADP, a compositional semantics for SADF based on Interactive Markov Chains (IMC) is introduced. Solutions are proposed to handle probabilistic choice and potentially unbounded buffers in CADP. The analysis approach based on CADP is illustrated on an MPEG-4 decoder. Starting from an SADF model of the decoder, the IMCs of each individual SADF actor are glued together by parallel composition. The resulting monolithic IMC is processed by hiding the synchronizations between individual IMCs, applying maximal progress, minimizing modulo branching bisimulation, and amalgamating probabilistic with subsequent Markovian transitions. The whole process, which was automated using SVL scripts, yields a Continuous-Time Markov Chain (CTMC) suitable for analysis. Several kinds of functional properties (reachability, occurrence, and response) of the MPEG-4 model were successfully analysed using CADP. As regards performance evaluation, besides transient and steady-state analysis on the CTMC of the decoder, CADP allowed to compute a more intricate performance measure, namely the response time distribution of the reconstruction (RC) component. This was carried out by modeling an observer to the IMC of the SADF component which synchronises on the first firing completion of the RC component. The time to reach the final state of the observer yielded the requested measure. In [Theelen-Katoen-Wu-12] is reported that: This form of analysis is not supported by SDF3, which only allows computing some statistics of the response time distribution being the minimum, maximum and expected response time. This shows the added value of using a model checking tool like CADP.
Conclusions:	Applying CADP for model checking SADF revealed several new insights compared to the SDF3 approach. Contemporary model checkers like CADP provide more flexibility over dedicated ones like SDF3, especially in terms of the range of analysable properties. On the other hand, SDF3 mostly supports reward-based properties that could not be evaluated with CADP. Due to the different time models of CADP and SDF3, it seems however difficult to fairly compare their effectiveness (in terms of quantitative analysis results) and efficiency (in terms of state space sizes).
Publications:	[Theelen-Katoen-Wu-12] Bart Theelen, Joost-Pieter Katoen, and Hao Wu. "Model Checking of Scenario-Aware Dataflow with CADP". Proceedings of Design, Automation and Test in Europe Conference and Exhibition DATE'2012 (Dresden, Germany), IEEE Computer Society Press, pages 653-658, March 2012. Available on-line at: ftp://ics.ele.tue.nl/pub/users/btheelen/Publications/Papers/DATE12.pdf or from the CADP Web site in PDF or PostScript
Contact:	Bart Theelen Embedded Systems Institute Laplace Building 0.10 Den Dolech 2 5612 AZ Eindhoven The Netherlands Tel: +31 (0)40 247 47 20 Fax: +31 (0)40 247 20 78 Email: Bart.Theelen@esi.nl
Further remarks:	This case study, amongst others, is described on the CADP Web site: http://cadp.inria.fr/case-studies

Back to the CADP case studies page