Correct-by-construction model-based design of reactive streaming software for multi-core embedded systems

  • Fotios GioulekasEmail author
  • Peter Poplavko
  • Panagiotis Katsaros
  • Saddek Bensalem
  • Pedro Palomo
FASE 2018


We present a model-based design approach toward correct-by-construction implementations of reactive streaming software for multi-core systems. A system’s implementation is derived from a high-level process network model by applying semantics-preserving model transformations. The so-called fixed priority process networks (FPPNs) are programmed independently from the execution platform and combine streaming and reactive control behavior with task parallelism for utilizing multi-core processing. We first define the FPPN sequential execution semantics that specifies precedence constraints between job executions of different tasks. Applications are thus rendered such that for any given test stimuli, a deterministic output response is expected. Furthermore, we define the FPPN real-time semantics based on a timed-automata modeling framework. This is provably a functionally equivalent semantics specifying the real-time execution of FPPNs and enabling runtime managers for scheduling jobs on multi-cores. A model transformation framework has been developed for deriving executable implementations of FPPNs on the BIP (Behavior–Interaction–Priority) runtime environment, ported on multi-core platforms. Schedulability is established by static analysis of the FPPN, and it is guaranteed by construction. Thus, the developers do not need to program low-level real-time OS services (e.g., for task management) and applications are amenable to testing, as opposed to if their outputs would depend on timing behavior. We have successfully ported a guidance-navigation and control application of a satellite system, onto a radiation hardened multi-core platform. Various implementation scenarios for efficiently utilizing HW resources are illustrated, and the test results are discussed.


Process network Model of computation Model transformation Timed-automata Critical systems Multi-core processors 



  1. 1.
    Abdellatif, T., Combaz, J., Sifakis, J.: Model-based implementation of real-time applications. In: Proceedings of the Tenth ACM International Conference on Embedded Software, EMSOFT ’10. ACM, New York, NY, USA, pp. 229–238 (2010).
  2. 2.
    Amnell, T., Fersman, E., Mokrushin, L., Pettersson, P., Yi, W.: Times: a tool for schedulability analysis and code generation of real-time systems. In: Larsen, K.G., Niebert, P. (eds.) Formal Modeling and Analysis of Timed Systems, pp. 60–72. Springer, Berlin (2004)CrossRefGoogle Scholar
  3. 3.
    Autofocus tool. [Available Online; accessed: 05-February-2019]
  4. 4.
    Baier, C., Katoen, J.P.: Principles of Model Checking (Representation and Mind Series). The MIT Press, Cambridge (2008)zbMATHGoogle Scholar
  5. 5.
    Basu, A., Bensalem, S., Bozga, M., Bourgos, P., Maheshwari, M., Sifakis, J.: Component assemblies in the context of manycore. In: Beckert, B., Damiani, F., de Boer, F.S., Bonsangue, M.M. (eds.) Formal Methods for Components and Objects: 10th International Symposium, FMCO 2011, Turin, Italy, October 3–5, 2011, Revised Selected Papers. Springer, Berlin, pp. 314–333 (2013)Google Scholar
  6. 6.
    Brau, G., Hugues, J., Navet, N.: Towards the systematic analysis of non-functional properties in model-based engineering for real-time embedded systems. Sci. Comput. Program. 156, 1–20 (2018). CrossRefGoogle Scholar
  7. 7.
    Broy, M., Dederichs, F., Dendorfer, C., Fuchs, M., Gritzner, T., Weber, R.: The design of distributed systems—an introduction to focus. Tech. Rep. TUM-I 9202-2, Technische Universitat Munchen (1992)Google Scholar
  8. 8.
    Broy, M., Stolen, K.: Systems: Focus on Streams, Interfaces, and Refinement, p. 348. Springer, New York (2001). zbMATHGoogle Scholar
  9. 9.
    Broy, M., Fox, J., Hölzl, F., Koss, D., Kuhrmann, M., Meisinger, M., Penzenstadler, B., Rittmann, S., Schätz, B., Spichkova, M., Wild, D.: Service-Oriented Modeling of CoCoME with Focus and AutoFocus, pp. 177–206. Springer, Berlin (2008). Google Scholar
  10. 10.
    Chaki, S., Kyle, D.: DMPL: Programming and verifying distributed mixed-synchrony and mixed-critical software. Tech. rep., Carnegie Mellon University (2016).
  11. 11.
    Claraz, D., Grimal, F., Laydier, T., Mader, R., Wirrer, G.: Introducing multi-core at automotive engine systems. In: ERTSS’14, Embedded Real-Time Software and Systems (2014)Google Scholar
  12. 12.
    Cordovilla, M., Boniol, F., Forget, J., Noulard, E., Pagetti, C.: Developing critical embedded systems on multicore architectures: the Prelude-SchedMCore toolset. In: RTNS (2011)Google Scholar
  13. 13.
    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. Proc. IEEE 91(1), 127–144 (2003)CrossRefGoogle Scholar
  14. 14.
    Feiler, P., Gluch, D., Hudak, J.: The architecture analysis & design language (AADL): an introduction. Tech. Rep. CMU/SEI-2006-TN-011, Software Engineering Institute, Carnegie Mellon University, Pittsburgh, PA (2006).
  15. 15.
    Forget, J., Boniol, F., Grolleau, E., Lesens, D., Pagetti, C.: Scheduling dependent periodic tasks without synchronization mechanisms. In: RTAS’10, pp. 301–310 (2010)Google Scholar
  16. 16.
    Fuhrmann, H., von Hanxleden, R., Rennhack, J., Koch, J.: Model-based system design of time-triggered architectures– -avionics case study. In: 2006 IEEE/AIAA 25th Digital Avionics Systems Conference, pp. 1–12 (2006).
  17. 17.
    Geilen, M., Basten, T.: Reactive process networks. In: EMSOFT’04. ACM, pp. 137–146 (2004)Google Scholar
  18. 18.
    Ghamarian, A.H.: Timing analysis of synchronous dataflow graphs. Ph.D. thesis, Eindhoven University of Technology (2008)Google Scholar
  19. 19.
    Giannopoulou, G., Poplavko, P., Socci, D., Huang, P., Stoimenov, N., Bourgos, P., Thiele, L., Bozga, M., Bensalem, S., Girbal, S., Faugere, M., Soulat, R., de Dinechin, B.D.: DOL-BIP-critical: a tool chain for rigorous design and implementation of mixed-criticality multi-core systems. Des. Autom. Embed. Syst. 22(1), 141–181 (2018). CrossRefGoogle Scholar
  20. 20.
    Gioulekas, F., Poplavko, P., Katsaros, P., Palomo, P.: Process network models for embedded system design based on the real-time bip execution engine. In: S. Bliudze, S. Bensalem (eds.) Proceedings of the 1st International Workshop on Methods and Tools for Rigorous System Design, Thessaloniki, Greece, 15th April 2018, Electronic Proceedings in Theoretical Computer Science, vol. 272. Open Publishing Association, pp. 79–92 (2018).
  21. 21.
    Gioulekas, F., Poplavko, P., Katsaros, P., Bensalem, S., Palomo, P.: A process network model for reactive streaming software with deterministic task parallelism. In: Russo, A., Schürr, A. (eds.) Fundamental Approaches to Software Engineering, pp. 94–110. Springer, Cham (2018). CrossRefGoogle Scholar
  22. 22.
    GR-CPCI-LEON4-N2X: Quad-core LEON4 next generation microprocessor evaluation board,
  23. 23.
    Ha, S., Kim, S., Lee, C., Yi, Y., Kwon, S., Joo, Y.P.: PeaCE: a hardware-software codesign environment for multimedia embedded systems. ACM Trans. Des. Autom. Electron. Syst. 12(3), 24:1–24:25 (2008)Google Scholar
  24. 24.
    Halbwachs, N.: Synchronous Programming of Reactive Systems. Springer, Berlin (2010)zbMATHGoogle Scholar
  25. 25.
    Hansson, A., Goossens, K., Bekooij, M., Huisken, J.: CoMPSoC: a template for composable and predictable multi-processor system on chips. ACM Trans. Des. Autom. Electron. Syst. (TODAES) 14(1), 2 (2009)Google Scholar
  26. 26.
    Hölzl, F., Feilkas, M.: 13 AutoFocus 3–A Scientific Tool Prototype for Model-Based Development of Component-Based, Reactive, Distributed Systems, pp. 317–322. Springer, Berlin (2010). Google Scholar
  27. 27.
    Huber, F., Molterer, S., Rausch, A., Schatz, B., Sihling, M., Slotosch, O.: Tool supported specification and simulation of distributed systems. In: B. Kramer, N. Uchihira, P. Croll, and S. Russo (eds.) International Symposium on Software Engineering for Parallel and Distributed Systems. IEEE, pp. 155–164 (1998)Google Scholar
  28. 28.
    Hugues, J., Zalila, B., Pautet, L., Kordon, F.: From the prototype to the final embedded system using the Ocarina AADL tool suite. ACM Trans. Embed. Comput. Syst. 7(4), 42:1–42:25 (2008)Google Scholar
  29. 29.
    Johnston, W.M., Hanna, J.R.P., Millar, R.J.: Advances in dataflow programming languages. ACM Comput. Surv. 36(1), 1–34 (2004)CrossRefGoogle Scholar
  30. 30.
    Kahn, G.: The semantics of a simple language for parallel programming. In: J.L. Rosenfeld (ed.) Information Processing ’74: Proceedings of the IFIP Congress. North-Holland, New York, NY, pp. 471–475 (1974)Google Scholar
  31. 31.
    Lee, E.A., Messerschmitt, D.G.: Static scheduling of synchronous data flow programs for digital signal processing. IEEE Trans. Comput. C–36(1), 24–35 (1987)CrossRefGoogle Scholar
  32. 32.
    Lee, E.A., Messerschmitt, D.G.: Synchronous data flow. Proc. IEEE 75(9), 1235–1245 (1987). CrossRefGoogle Scholar
  33. 33.
    Mkaouar, H., Zalila, B., Hugues, J., Jmaiel, M.: From AADL model to LNT specification. In: Reliable Software Technologies—Ada-Europe 2015. Springer, Cham, pp. 11–20 (2015).
  34. 34.
    Perrotin, M., Conquet, E., Delange, J., Schiele, A., Tsiodras, T.: TASTE: a real-time software engineering tool-chain overview, status, and future. In: I. Ober, I. Ober (eds.) SDL 2011: Integrating System and Software Modeling. International SDL Forum. Revised Papers. Springer, Berlin, pp. 26–37 (2012)Google Scholar
  35. 35.
    Poplavko, P., Kahil, R., Socci, D., Bensalem, S., Bozga, M.: Mixed-critical systems design with coarse-grained multi-core interference. In: Leveraging Applications of Formal Methods, Verification and Validation: Foundational Techniques, ISoLA’16. Springer, pp. 605–621 (2016).
  36. 36.
    Poplavko, P., Nouri, A., Angelis, L., Zerzelidis, A., Bensalem, S., Katsaros, P.: Regression-based statistical bounds on software execution time. In: Verification and Evaluation of Computer and Communication Systems—11th International Conference, VECoS 2017, Montreal, QC, Canada, August 24–25, 2017, Proceedings, pp. 48–63 (2017).
  37. 37.
    Poplavko, P., Socci, D., Bourgos, P., Bensalem, S., Bozga, M.: Models for deterministic execution of real-time multiprocessor applications. In: Proceedings of the 2015 Design, Automation and Test in Europe Conference and Exhibition, DATE ’15. EDA Consortium, San Jose, CA, USA, pp. 1665–1670 (2015).
  38. 38.
    Saidi, S.: On the benefits of multicores for real-time systems. In: 2017 Euromicro Conference on Digital System Design (DSD), pp. 383–389 (2017).
  39. 39.
    Socci, D., Poplavko, P., Bensalem, S., Bozga, M.: A timed-automata based middleware for time-critical multicore applications. In: 2015 IEEE International Symposium on Object/Component/Service-Oriented Real-Time Distributed Computing Workshops, pp. 1–8 (2015).
  40. 40.
    Time-critical applications on multicore platforms.
  41. 41.
    Triki, A., Combaz, J., Bensalem, S., Sifakis, J.: Model-based implementation of parallel real-time systems. In: Proceedings of the 16th International Conference on Fundamental Approaches to Software Engineering, FASE’13. Springer, Berlin, pp. 235–249 (2013)Google Scholar
  42. 42.
    Waez, M.T.B., Dingel, J., Rudie, K.: A survey of timed automata for the development of real-time systems. Comput. Sci. Rev. 9, 1–26 (2013)CrossRefzbMATHGoogle Scholar
  43. 43.
    Yang, Z., Hu, K., Ma, D., Pi, L.: Towards a formal semantics for the AADL behavior annex. In: 2009 Design, Automation Test in Europe Conference Exhibition, pp. 1166–1171 (2009).
  44. 44.
    Yang, Z., Hu, K., Ma, D., Bodeveix, J.P., Pi, L., Talpin, J.P.: From aadl to timed abstract state machines: a verified model transformation. J. Syst. Softw. 93, 42–68 (2014). CrossRefGoogle Scholar

Copyright information

© Springer-Verlag GmbH Germany, part of Springer Nature 2019

Authors and Affiliations

  • Fotios Gioulekas
    • 1
    Email author
  • Peter Poplavko
    • 2
  • Panagiotis Katsaros
    • 1
  • Saddek Bensalem
    • 3
  • Pedro Palomo
    • 4
  1. 1.Department of InformaticsAristotle University of ThessalonikiThessalonikiGreece
  2. 2.Mentor®. A Siemens BusinessMontbonnotFrance
  3. 3.VERIMAGUniversité Grenoble Alpes (UGA)GrenobleFrance
  4. 4.Deimos-Space®MadridSpain

Personalised recommendations