Performance model checking scenario-aware dataflow
conference paper
Dataflow formalisms are useful for specifying signal processing and streaming applications. To adequately capture the dynamic aspects of modern applications, the formalism of Scenario-Aware Dataflow (SADF) was recently introduced, which allows analysis of worst/best-case and average-case performance across different modes of operation (scenarios). The semantic model of SADF integrates non-deterministic and discrete probabilistic behaviour with generic discrete time distributions. This combination is different from the semantic models underlying contemporary quantitative model checking approaches, which often assume exponentially distributed or continuous time or they lack support for expressing discrete probabilistic behaviour. This paper discusses a model-checking approach for computing quantitative properties of SADF models such as throughput, time-weighted average buffer occupancy and maximum response time. A compositional state-space reduction technique is introduced as well as an efficient implementation of this method that combines model construction with on-the-fly state-space reductions. Strong reductions are possible because of special semantic properties of SADF, which are common to dataflow models. We illustrate this efficiency with several case studies from the multi-media domain.
Topics
Average-caseBuffer occupancyContinuous timeDataflow modelDifferent modesDiscrete timeDynamic aspectsEfficient implementationMaximum response timeModel constructionModern applicationsMulti-MediaOn-the-flyPerformance ModelQuantitative model checkingSemantic ModelSemantic propertiesState-space reductionStreaming applicationsTime-weighted averagesModel checkingProbability distributionsSemanticsSignal processingTime sharing systemsData flow analysis
TNO Identifier
954253
ISSN
03029743
ISBN
9783642243
Publisher
Springer
Source title
Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 9th International Conference on Formal Modeling and Analysis of Timed Systems, FORMATS 2011, 21 September 2011 through 23 September 2011
Pages
43-59
Files
To receive the publication files, please send an e-mail request to TNO Repository.