Automated Conflict-Free Concurrent Implementation of Timed Component-Based Models

  • Ahlem TrikiEmail author
  • Borzoo Bonakdarpour
  • Jacques Combaz
  • Saddek Bensalem
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 9058)


Correct implementation of concurrent real-time systems has always been a tedious task due to their inherent complex structure; concurrency introduces a great deal of non-determinism, which can potentially conflict with meeting timing constraints. In this paper, we focus on model-based concurrent implementation of timed models. Our abstract models consist of a set of components interacting with each other using multi-party interactions. Each component is internally subject to a set of timing constraints. We propose a chain of transformations that starts with an abstract model as input and generates correct-by-construction executable code as output. We show that all transformed models are observationally equivalent to the abstract model through bisimulation proofs and, hence, all functional properties of the abstract model are preserved. To facilitate developing the proofs of correctness, each transformation obtains a model by incorporating a subset of physical constraints (e.g., type of communication and global clock synchronization)


Timing Constraint Abstract Model Label Transition System Interaction Protocol Atomic Component 
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.
    Abdellatif, T., Combaz, J., Sifakis, J.: Model-based implementation of real-time applications. In: ACM International Conference on Embedded Software (EMSOFT), pp. 229–238 (2010)Google Scholar
  2. 2.
    Alur, R., Dill, D.: A theory of timed automata. Theoretical Computer Science 126(2), 183–235 (1994)CrossRefzbMATHMathSciNetGoogle Scholar
  3. 3.
    Amnell, T., Fersman, E., Mokrushin, L., Pettersson, P., Yi, W.: TIMES - a tool for modelling and implementation of embedded systems. In: Katoen, J.-P., Stevens, P. (eds.) Tools and Algorithms for the Construction and Analysis of Systems (TACAS). LNCS, vol. 2280, pp. 460–464. Springer, Heidelbeeg (2002)CrossRefGoogle Scholar
  4. 4.
    Basu, A., Bidinger, P., Bozga, M., Sifakis, J.: Distributed semantics and implementation for systems with interaction and priority. In: Suzuki, K., Higashino, T., Yasumoto, K., El-Fakih, K. (eds.) FORTE. LNCS, vol. 5048, pp. 116–133. Springer, Heidelberg (2008)Google Scholar
  5. 5.
    Basu, A., Bozga, M., Sifakis, J.: Modeling heterogeneous real-time components in BIP. In: Software Engineering and Formal Methods (SEFM), pp. 3–12 (2006)Google Scholar
  6. 6.
    Bliudze, S., Sifakis, J.: A notion of glue expressiveness for component-based systems. In: Bliudze, S., Sifakis, J. (eds.) Concurrency Theory (CONCUR). LNCS, vol. 5201, pp. 508–522. Springer, Heidelberg (2008)Google Scholar
  7. 7.
    Bonakdarpour, B., Bozga, M., Jaber, M., Quilbeuf, J., Sifakis, J.: A framework for automated distributed implementation of component-based models. Springer Journal on Distributed Computing (DC) 25(1), 383–409 (2012)CrossRefzbMATHGoogle Scholar
  8. 8.
    Bonakdarpour, B., Bozga, M., Quilbeuf, J.: Automated distributed implementation of component-based models with priorities. In: ACM International Conference on Embedded Software (EMSOFT), pp. 59–68 (2011)Google Scholar
  9. 9.
    Daws, C., Yovine, S.: Reducing the number of clock variables of timed automata. In: RTSS, pp. 73–81. IEEE Computer Society (1996)Google Scholar
  10. 10.
    ISO/IEC. Information Processing Systems - Open Systems Interconnection: LOTOS, A Formal Description Technique Based on the Temporal Ordering of Observational Behavior (1989)Google Scholar
  11. 11.
    Jee, E., Wang, S., Kim, J.-K., Lee, J., Sokolsky, O., Lee, I.: A safety-assured development approach for real-time software. In: Proceedings of the 16th IEEE International Conference on Embedded and Real-Time Computing Systems and Applications (RTCSA), pp. 133–142 (2010)Google Scholar
  12. 12.
    Murata, T.: Petri nets: Properties, analysis and applications. Proceedings of the IEEE 77(4), 541–580 (1989)CrossRefGoogle Scholar
  13. 13.
    Tauber, J.A., Lynch, N.A., Tsai, M.J.: Compiling IOA without global synchronization. In: Symposium on Network Computing and Applications (NCA), pp. 121–130 (2004)Google Scholar
  14. 14.
    Triki, A., Bonakdarpoor, B., Combaz, J., Bensalem, S.: Automated conflict-free concurrent implementation of timed component-based models. Technical report, Verimag Research ReportGoogle Scholar
  15. 15.
    Triki, A., Combaz, J., Bensalem, S., Sifakis, J.: Model-based implementation of parallel real-time systems. In: Cortellessa, V., Varró, D. (eds.) FASE. LNCS, vol. 7793, pp. 235–249. Springer, Heidelberg (2013)Google Scholar
  16. 16.
    von Bochmann, G., Gao, Q., Wu, C.: On the distributed implementation of lotos. In: FORTE, pp. 133–146 (1989)Google Scholar

Copyright information

© Springer International Publishing Switzerland 2015

Authors and Affiliations

  • Ahlem Triki
    • 1
    Email author
  • Borzoo Bonakdarpour
    • 2
  • Jacques Combaz
    • 1
  • Saddek Bensalem
    • 1
  1. 1.University Grenoble Alpes/CNRS, VERIMAGGrenobleFrance
  2. 2.McMaster UniversityHamiltonCanada

Personalised recommendations