Embedded Systems Institute, Eindhoven (THE NETHERLANDS)
RWTH Aachen (GERMANY)
CADP (Construction and Analysis of Distributed Processes)
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:
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
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
Embedded Systems Institute
Laplace Building 0.10
Den Dolech 2
5612 AZ Eindhoven
Tel: +31 (0)40 247 47 20
Fax: +31 (0)40 247 20 78
|Further remarks:||This case study, amongst others, is described on the CADP Web site: http://cadp.inria.fr/case-studies|