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.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
de Alfaro, L.: Formal Verification of Probabilistic Systems. PhD Thesis. Stanford University (1997)
Billingsley, P.: Probability and Measure, 2nd edn. Wiley, Chichester (1995)
Chaki, S., Clarke, E.M., Ouaknine, J., Sharygina, N., Sinha, N.: State/Event-Based Software Model Checking. In: Boiten, E.A., Derrick, J., Smith, G.P. (eds.) IFM 2004. LNCS, vol. 2999, pp. 128–147. Springer, Heidelberg (2004)
Chung, K.L.: Markov Chains with Stationary Transition Probabilities. Springer, Heidelberg (1967)
Derman, C.: Finite State Markovian Decision Processes. Academic Press, London (1970)
Geilen, M.C.W., Stuijk, S.: Worst-case Performance Analysis of Synchronous Dataflow Scenarios. In: Proceedings of CODES+ISSS 2010, pp. 125–134 (2010)
Govindarajan, R., Gao, G.R.: Rate-Optimal Schedule for Multi-Rate DSP Computations. Journal of VLSI Signal Processing 9, 211–235 (1995)
Ghamarian, A.H., Geilen, M.C.W., Stuijk, S., Basten, T., Moonen, A.J.M., Bekooij, M.J.G., Theelen, B.D., Mousavi, M.R.: Throughput Analysis of Synchronous Data Flow Graphs. In: Proceedings of ACSD 2006, pp. 25–34 (2006)
Ghamarian, A.H., Stuijk, S., Basten, T., Geilen, M.C.W., Theelen, B.D.: Latency Minimization for Synchronous Data Flow Graphs. In: Proceedings of DSD 2007, pp. 189–196 (2007)
Gheorghita, S.V., Stuijk, S., Basten, T., Corporaal, H.: Automatic Scenario Detection for Improved WCET Estimation. In: Proceedings of DAC 2005, pp. 101–104 (2005)
Gheorghita, S.V., Basten, T., Corporaal, H.: Application Scenarios in Streaming-Oriented Embedded System Design. In: Proceeedings of SoC 2006, pp. 175–178 (2006)
Garavel, H., Lang, F., Mateescu, R., Serwe, W.: CADP 2010: A Toolbox for the Construction and Analysis of Distributed Processes. In: Abdulla, P.A., Leino, K.R.M. (eds.) TACAS 2011. LNCS, vol. 6605, pp. 372–387. Springer, Heidelberg (2011)
Hermanns, H. (ed.): Interactive Markov Chains. LNCS, vol. 2428. Springer, Heidelberg (2002)
Katoen, J.-P., Hahn, E.M., Hermanns, H., Jansen, D., Zapreev, I.: The Ins and Outs of the Probabilistic Model Checker MRMC. In: Proceedings of QEST 2009, pp. 167–176 (2009)
Kwiatkowska, M., Norman, G., Parker, D.: PRISM 4.0: Verification of Probabilistic Real-time Systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 585–591. Springer, Heidelberg (2011)
Kwiatkowska, M., Norman, G., Parker, D., Sproston, J.: Performance Analysis of Probabilistic Timed Automata using Digital Clocks. Formal Methods in System Design 29, 33–78 (2006)
Larsen, K., Pettersson, P., Yi, W.: UPPAAL in a Nutshell. International Journal on Software Tools for Technology Transfer 1(1-2), 134–152 (1997)
Larsen, K.G., Yi, W.: Time abstracted bisimulation: Implicit specifications and decidability. Information and Communication 134, 75–103 (1997)
Lee, E., Messerschmitt, D.: Synchronous Data Flow. IEEE Proceedings 75(9), 1235–1245 (1987)
Moonen, A., Bekooij, M., van den Berg, R., van Meerbergen, J.: Practical and Accurate Throughput Analysis with the Cyclo Static Dataflow Model. In: Proceedings of MASCOTS 2007, pp. 238–245. IEEE, Los Alamitos (2007)
de Nicola, R., Vaandrager, F.W.: Action versus state based logics for transition systems. In: Guessarian, I. (ed.) LITP 1990. LNCS, vol. 469, pp. 407–419. Springer, Heidelberg (1990)
Nicollin, X., Sifakis, J.: An Overview of Synthesis on Timed Process Algebras. In: Larsen, K.G., Skou, A. (eds.) CAV 1991. LNCS, vol. 575, pp. 376–398. Springer, Heidelberg (1992)
Obal, W.D., Sanders, W.H.: State-Space Support for Path-Based Reward Variables. Performance Evaluation 35(3/4), 233–251 (1999)
Puterman, M.L.: Markov Decesion Processes. Wiley, Chichester (1995)
Poplavko, P., Basten, T., van Meerbergen, J.: Execution-Time Prediction for Dynamic Streaming Applications with Task-Level Parallelism. In: Proceedings of DSD 2007, pp. 228–235. IEEE, Los Alamitos (2007)
Segala, R.: Modeling and Verification of Randomized Distributed Real-Time Systems. PhD Thesis. Massachusetts Institute of Technology (1995)
Siram, S., Bhattacharyya, S.S.: Embedded Multiprocessors; Scheduling and Synchronization, 2nd edn. CRC Press, Boca Raton (2009)
Sokolova, A.: Coalgebraic Analysis of Probabilistic Systems. PhD Thesis. Eindhoven University of Technology (2005)
Stuijk, S., Geilen, M.C.W., Basten, T.: SDF3: SDF For Free. In: Proceedings of ACSD 2006, pp. 276–278 (2006)
Tijms, H.C.: Stochastic Models; An Algorithmic Approach. John Wiley & Sons, Chichester (1994)
Theelen, B.D.: Performance Modelling for System-Level Design. Ph.D. Thesis. Eindhoven University of Technology (2004)
Theelen, B.D.: A Performance Analysis Tool for Scenario-Aware Streaming Applications. In: Proceedings of QEST 2007 (2007)
Theelen, B.D., Geilen, M.C.W., Basten, T., Voeten, J.P.M., Gheorghita, S.V., Stuijk, S.: A Scenario-Aware Data Flow Model for Combined Long-Run Average and Worst-Case Performance Analysis. In: Proceedings of MEMOCODE 2006, pp. 185–194 (2006)
Theelen, B.D., Geilen, M.C.W., Stuijk, S., Gheorghita, S.V., Basten, T., Voeten, J.P.M., Ghamarian, A.H.: Scenario-Aware Dataflow. Technical Report ESR-2008-08, Eindhoven University of Technology (July 2008)
Voeten, J.P.M.: Performance Evaluation with Temporal Rewards. Performance Evaluation 50(2/3), 189–218 (2002)
Yi, W.: Real-time behaviour of asynchronous agents. In: Baeten, J.C.M., Klop, J.W. (eds.) CONCUR 1990. LNCS, vol. 458, pp. 502–520. Springer, Heidelberg (1990)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2011 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Theelen, B., Geilen, M., Voeten, J. (2011). Performance Model Checking Scenario-Aware Dataflow. In: Fahrenberg, U., Tripakis, S. (eds) Formal Modeling and Analysis of Timed Systems. FORMATS 2011. Lecture Notes in Computer Science, vol 6919. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-24310-3_5
Download citation
DOI: https://doi.org/10.1007/978-3-642-24310-3_5
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-24309-7
Online ISBN: 978-3-642-24310-3
eBook Packages: Computer ScienceComputer Science (R0)