Component Assemblies in the Context of Manycore

  • Ananda Basu
  • Saddek Bensalem
  • Marius Bozga
  • Paraskevas Bourgos
  • Mayur Maheshwari
  • Joseph Sifakis
Part of the Lecture Notes in Computer Science book series (LNCS, volume 7542)


We present a component-based software design flow for building parallel applications running on top of manycore platforms. The flow is based on the BIP - Behaviour, Interaction, Priority - component framework and its associated toolbox. It provides full support for modeling of application software, validation of its functional correctness, modeling and performance analysis on system-level models, code generation and deployment on target manycore platforms. The paper details some of the steps of the design flow. The design flow is illustrated through the modeling and deployment of two applications, the Cholesky factorization and the MJPEG decoding on MPARM, an ARM-based manycore platform. We emphasize the merits of the design flow, notably fast performance analysis as well as code generation and efficient deployment on manycore platforms.


Model Check Application Software Cholesky Factorization Total Execution Time Label Transition System 
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.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
  2. 2.
    Abadi, M., Lamport, L.: Conjoining specifications. ACM Transactions on Programming Languages and Systems 17(3), 507–534 (1995)CrossRefGoogle Scholar
  3. 3.
    Abdeddaim, Y., Asarin, E., Maler, O.: Scheduling with Timed Automata. Theoretical Computer Science 354, 272–300 (2006)MathSciNetCrossRefzbMATHGoogle Scholar
  4. 4.
    Henia, R., et al.: System-level performance analysis - the SymTA/S approach. In: IEEE Proceedings Computers and Digital Techniques, vol. 152, pp. 148–166 (2005)Google Scholar
  5. 5.
    Alur, R., Henzinger, T.: Reactive modules. In: Proceedings of LICS 1996, pp. 207–218. IEEE Computer Society Press (1996)Google Scholar
  6. 6.
    Basu, A., Bozga, M., Sifakis, J.: Modeling Heterogeneous Real-time Systems in BIP. In: Proceedings of SEFM 2006, pp. 3–12. IEEE Computer Society Press (2006)Google Scholar
  7. 7.
    Basu, A., Bensalem, S., Bozga, M., Caillaud, B., Delahaye, B., Legay, A.: Statistical Abstraction and Model-Checking of Large Heterogeneous Systems. In: Hatcliff, J., Zucca, E. (eds.) FMOODS/FORTE 2010, Part II. LNCS, vol. 6117, pp. 32–46. Springer, Heidelberg (2010)CrossRefGoogle Scholar
  8. 8.
    Basu, A., Bensalem, S., Bozga, M., Combaz, J., Jaber, M., Nguyen, T.H., Sifakis, J.: Rigorous component-based design using the BIP framework. IEEE Software, Special Edition – Software Components beyond Programming – from Routines to Services 28(3), 41–48 (2011)Google Scholar
  9. 9.
    Benini, L., Bertozzi, D., Bogliolo, A., Menichelli, F., Olivieri, M.: MPARM: Exploring the Multi-Processor SoC Design Space with SystemC. Journal of VLSI Signal Processing Systems 41, 169–182 (2005)CrossRefGoogle Scholar
  10. 10.
    Bensalem, S., Bozga, M., Sifakis, J., Nguyen, T.-H.: Compositional Verification for Component-Based Systems and Application. In: Cha, S(S.), Choi, J.-Y., Kim, M., Lee, I., Viswanathan, M. (eds.) ATVA 2008. LNCS, vol. 5311, pp. 64–79. Springer, Heidelberg (2008)CrossRefGoogle Scholar
  11. 11.
    Bensalem, S., Bozga, M., Nguyen, T.-H., Sifakis, J.: D-Finder: A Tool for Compositional Deadlock Detection and Verification. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 614–619. Springer, Heidelberg (2009)CrossRefGoogle Scholar
  12. 12.
    Bensalem, S., Lakhnech, Y.: Automatic generation of invariants. FMSD 15(1), 75–92 (1999)Google Scholar
  13. 13.
    Bensalem, S., Bozga, M., Legay, A., Nguyen, T.H., Sifakis, J., Yan, R.: Incremental Component-based Construction and Verification using Invariants. In: Proceedings of FMCAD 2010, pp. 257–266. IEEE (2010)Google Scholar
  14. 14.
    Bonakdarpour, B., Bozga, M., Jaber, M., Quilbeuf, J., Sifakis, J.: A Framework for Automated Distributed Implementation of Component-based Models. Distributed Computing (to appear, 2012)Google Scholar
  15. 15.
    Bourgos, P., Basu, A., Bozga, M., Bensalem, S., Sifakis, J., Huang, K.: Rigorous system level modeling and analysis of mixed HW/SW systems. In: Proceedings of MEMOCODE 2011, pp. 11–20. IEEE/ACM (2011)Google Scholar
  16. 16.
    Chandy, K., Misra, J.: Parallel program design: a foundation. Addison-Wesley Publishing Company (1988)Google Scholar
  17. 17.
    Clarke, E., Long, D., McMillan, K.: Compositional model checking. In: Proceedings of LICS 1989, pp. 353–362 (1989)Google Scholar
  18. 18.
    Eker, J., Janneck, J.W., Lee, E.A., Liu, J., Liu, X., Ludvig, J., Neuendorffer, S., Sachs, S., Xiong, Y.: Taming heterogeneity: The Ptolemy approach. Proceedings of the IEEE 91(1), 127–144 (2003)CrossRefGoogle Scholar
  19. 19.
    Erbas, C., Pimentel, A.D., Thompson, M., Polstra, S.: A framework for system-level modeling and simulation of embedded systems architectures. EURASIP Journal on Embedded Systems 2007 (2007)Google Scholar
  20. 20.
    Feiler, P.H., Lewis, B., Vestal, S.: The SAE Architecture Analysis and Design Language (AADL) Standard: A basis for model-based architecture-driven embedded systems engineering. In: Proceedings of RTAS Workshop on Model-driven Embedded Systems, pp. 1–10 (2003)Google Scholar
  21. 21.
    Grumberg, O., Long, D.E.: Model checking and modular verification. ACM Transactions on Programming Languages and Systems 16(3), 843–871 (1994)CrossRefGoogle Scholar
  22. 22.
    Kienhuis, B., Deprettere, E., Vissers, K., van der Wolf, P.: An approach for quantitative analysis of application-specific dataflow architectures. In: Proceedings of ASAP 1997, pp. 338–349. IEEE Computer Society (1997)Google Scholar
  23. 23.
    Künzli, S., Poletti, F., Benini, L., Thiele, L.: Combining Simulation and Formal Methods for System-level Performance Analysis. In: Proceedings of DATE 2006, pp. 236–241 (2006)Google Scholar
  24. 24.
    Kupferman, O., Vardi, M.Y.: Modular Model Checking. In: de Roever, W.-P., Langmaack, H., Pnueli, A. (eds.) COMPOS 1997. LNCS, vol. 1536, pp. 381–401. Springer, Heidelberg (1998)CrossRefGoogle Scholar
  25. 25.
    Leary, D.P., Stewart, G.: Data-flow algorithms for parallel matrix computations. Communications of the ACM 28(8), 840–853 (1985)MathSciNetCrossRefzbMATHGoogle Scholar
  26. 26.
    Lieverse, P., Stefanov, T., van der Wolf, P., Deprettere, E.: System level design with SPADE: an M-JPEG case study. In: ICCAD, pp. 31–38 (2001)Google Scholar
  27. 27.
    McMillan, K.L.: A Compositional Rule for Hardware Design Refinement. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol. 1254, pp. 24–35. Springer, Heidelberg (1997)CrossRefGoogle Scholar
  28. 28.
    Moussa, I., Grellier, T., Nguyen, G.: Exploring SW Performance Using SoC Transaction-Level Modeling. In: Proceedings of DATE 2003, pp. 20120–20125 (2003)Google Scholar
  29. 29.
    Nikolov, H., Thompson, M., Stefanov, T., Pimentel, A., Polstra, S., Bose, R., Zissulescu, C., Deprettere, E.: Daedalus: toward composable multimedia mp-soc design. In: Proceedings of DAC 2008, pp. 574–579. ACM (2008)Google Scholar
  30. 30.
    OMG: OMG Systems Modeling Language SysML (OMG SysML). Object Management Group (2008)Google Scholar
  31. 31.
    Pnueli, A.: In transition from global to modular temporal reasoning about programs, pp. 123–144 (1985)Google Scholar
  32. 32.
    PRO3D: Programming for Future 3D Architecture with Many Cores, FP7 project funded by the EU under grant agreement 248 776,
  33. 33.
    Salah, R.B., Bozga, M., Maler, O.: Compositional Timing Analysis. In: Proceedings of EMSOFT 2009, pp. 39–48 (2009)Google Scholar
  34. 34.
    Stark, E.W.: A Proof Technique for Rely/Guarantee Properties. In: Maheshwari, S.N. (ed.) FSTTCS 1985. LNCS, vol. 206, pp. 369–391. Springer, Heidelberg (1985)CrossRefGoogle Scholar
  35. 35.
    Thiele, L., Bacivarov, I., Haid, W., Huang, K.: Mapping Applications to Tiled Multiprocessor Embedded Systems. In: Proceedings of ACSD 2007, pp. 29–40. IEEE Computer Society (2007)Google Scholar
  36. 36.
    Thiele, L., Chakraborty, S., Naedele, M.: Real-time calculus for scheduling hard real-time systems. In: Proceedings of ISCAS 2002, vol. 4, pp. 101–104. IEEE (2002)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2013

Authors and Affiliations

  • Ananda Basu
    • 1
  • Saddek Bensalem
    • 1
  • Marius Bozga
    • 1
  • Paraskevas Bourgos
    • 1
  • Mayur Maheshwari
    • 1
  • Joseph Sifakis
    • 1
    • 2
  1. 1.VERIMAG UMR 5104UJF-Grenoble 1 / CNRSGrenobleFrance
  2. 2.RISD LaboratoryEPFLSwitzerland

Personalised recommendations