Performance model checking scenario-aware dataflow

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

9 Citations (Scopus)
2 Downloads (Pure)

Abstract

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.
Original languageEnglish
Title of host publicationProceedings of the 9th International Conference on Formal Modeling and Analysis of Timed Systems (FORMATS'11), 21-23 September 2011, Aalborg, Denmark,
EditorsS. Tripakis U. Fahrenberg
Place of PublicationBerlin
PublisherSpringer
Pages43-59
ISBN (Print)978-3-642-24309-7
DOIs
Publication statusPublished - 2011
Eventconference; 9th International Conference on Formal Modeling and Analysis of Timed Systems (FORMATS'11); 2011-09-21; 2011-09-23 -
Duration: 21 Sep 201123 Sep 2011

Publication series

NameLecture Notes in Computer Science
Volume6919
ISSN (Print)0302-9743

Conference

Conferenceconference; 9th International Conference on Formal Modeling and Analysis of Timed Systems (FORMATS'11); 2011-09-21; 2011-09-23
Period21/09/1123/09/11
Other9th International Conference on Formal Modeling and Analysis of Timed Systems (FORMATS'11)

Fingerprint Dive into the research topics of 'Performance model checking scenario-aware dataflow'. Together they form a unique fingerprint.

  • Cite this

    Theelen, B. D., Geilen, M. C. W., & Voeten, J. P. M. (2011). Performance model checking scenario-aware dataflow. In S. T. U. Fahrenberg (Ed.), Proceedings of the 9th International Conference on Formal Modeling and Analysis of Timed Systems (FORMATS'11), 21-23 September 2011, Aalborg, Denmark, (pp. 43-59). (Lecture Notes in Computer Science; Vol. 6919). Springer. https://doi.org/10.1007/978-3-642-24310-3_5