Towards Performance Prediction of Compositional Models in Industrial GALS Designs

  • Nicolas Coste
  • Holger Hermanns
  • Etienne Lantreibecq
  • Wendelin Serwe
Part of the Lecture Notes in Computer Science book series (LNCS, volume 5643)


Systems and Networks on Chips (NoCs) are a prime design focus of many hardware manufacturers. In addition to functional verification, which is a difficult necessity, the chip designers are facing extremely demanding performance prediction challenges, such as the need to estimate the latency of memory accesses over the NoC. This paper attacks this problem in the setting of designing globally asynchronous, locally synchronous systems (GALS). We describe foundations and applications of a combination of compositional modeling, model checking, and Markov process theory, to arrive at a viable approach to compute performance quantities directly on industrial, functionally verified GALS models.


Performance Prediction Markov Decision Process Operational Semantic Steady State Probability Virtual Channel 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


  1. 1.
    Coste, N., Garavel, H., Hermanns, H., Hersemeule, R., Thonnart, Y., Zidouni, M.: Quantitative evaluation in embedded system design: Validation of multiprocessor multithreaded architectures. In: DATE (March 2008)Google Scholar
  2. 2.
    Garavel, H., Lang, F., Mateescu, R., Serwe, W.: CADP 2006: A toolbox for the construction and analysis of distributed processes. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol. 4590, pp. 158–163. Springer, Heidelberg (2007)CrossRefGoogle Scholar
  3. 3.
    Hansson, H.A.: Time and Probability in Formal Design of Distributed Systems. Elsevier Science, Amsterdam (1994)Google Scholar
  4. 4.
    Hermanns, H. (ed.): Interactive Markov Chains. LNCS, vol. 2428. Springer, Heidelberg (2002)zbMATHGoogle Scholar
  5. 5.
    Hermanns, H., Lohrey, M.: Priority and maximal progress are completely axiomatisable (extended abstract). In: Sangiorgi, D., de Simone, R. (eds.) CONCUR 1998. LNCS, vol. 1466, pp. 237–252. Springer, Heidelberg (1998)CrossRefGoogle Scholar
  6. 6.
    ISO/IEC. LOTOS — a formal description technique based on the temporal ordering of observational behaviour. International Standard 8807 (1989)Google Scholar
  7. 7.
    Jonsson, B., Yi, W., Larsen, K.G.: Probabilistic Extensions of Process Algebras, ch. 11, pp. 685–710. North Holland, Amsterdam (2001)zbMATHGoogle Scholar
  8. 8.
    Larsen, K.G., Skou, A.: Compositional verification of probabilistic processes. In: Cleaveland, W.R. (ed.) CONCUR 1992. LNCS, vol. 630, pp. 456–471. Springer, Heidelberg (1992)CrossRefGoogle Scholar
  9. 9.
    Nicollin, X., Sifakis, J.: An overview and synthesis on timed process algebras. In: Larsen, K.G., Skou, A. (eds.) CAV 1991. LNCS, vol. 575, pp. 376–398. Springer, Heidelberg (1992)CrossRefGoogle Scholar
  10. 10.
    Nicollin, X., Sifakis, J.: The algebra of timed processes ATP: Theory and application. Information and Computation 114(1), 131–178 (1994)MathSciNetCrossRefzbMATHGoogle Scholar
  11. 11.
    Puterman, M.L.: Markov Decision Processes. Wiley, Chichester (1994)CrossRefzbMATHGoogle Scholar
  12. 12.
    Swartz, K.L., Cottrell, R.L., Dart, M.: Adventures in the evolution of a high-bandwidth network for central servers. In: LISA. USENIX (1994)Google Scholar
  13. 13.
    Trčka, N., Georgievska, S.: Branching bisimulation congruence for probabilistic systems. In: QAPL 2008. Electronic Notes in Theoretical Computer Science, vol. 220, pp. 129–143 (2008)Google Scholar
  14. 14.
    van Glabbeek, R.J., Weijland, W.P.: Branching time and abstraction in bisimulation semantics (extended abstract). In: IFIP congress, pp. 613–618 (1989)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2009

Authors and Affiliations

  • Nicolas Coste
    • 1
    • 2
  • Holger Hermanns
    • 1
    • 3
  • Etienne Lantreibecq
    • 2
  • Wendelin Serwe
    • 1
  1. 1.INRIA Grenoble – Rhône-Alpes, VASY project teamFrance
  2. 2.STMicroelectronics GrenobleFrance
  3. 3.Universität des SaarlandesGermany

Personalised recommendations