Formal Support for Untimed MARTE-SystemC Interoperability

Conference paper
Part of the Lecture Notes in Electrical Engineering book series (LNEE, volume 106)


Model-Driven Architecture (MDA) and Electronic System Level (ESL) design are key approaches for succeeding in the specification and design of current embedded systems, which are increasingly complex and heterogeneous. MARTE is the most advanced UML profile for abstract specification of real-time embedded systems in the MDA context, while SystemC is the language most widely adopted by the ESL design community. Nevertheless, SystemC lacks well defined formal semantics for abstract specification, specifically for untimed models. This paper tackles this problem by providing the fundamentals of a framework which enables the analysis of the MARTE model and the corresponding SystemC specification under a formal meta-model. Based on this formal meta-model, formal support for a consistent and synergistic link between MARTE and SystemC is provided. This support is based on ForSyDe. The ForSyDe formalism is used as a formal framework for untimed SystemC models and to reflect the abstract execution semantics of both the MARTE model and its corresponding SystemC executable specification. Thus, the conditions for the SystemC specification to correspond to its formal meta-model are defined. The concepts introduced are shown through the specification of an essential part of a video decoder.


Shared Variable Activity Diagram Formal Support Abstract State Machine Execution Semantic 
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.
    OMG: “MDA guide, Version 1.1”,, 2003.
  2. 2.
    B. Bailey, G. Martin and A. Piziali: “ESL Design and Verification”, Morgan Kaufman, 2007.Google Scholar
  3. 3.
    OMG: “UML 2.1 Superstructure Specification”,, 2006.
  4. 4.
    L. Lavagno, G. Martin, B. Selic (Eds.): “UML for real: design of embedded real-time systems”, Springer, 2003.Google Scholar
  5. 5.
    OMG: “UML Profile for MARTE, v1.0”,, 2009.
  6. 6.
    S. Taha, A. Radermacher, S. Gerard and Jean-Luc Dekeeyser: “MARTE: UML-based Hardware Design from Modeling to Simulation”, in proc. of FDL’2007, ECSI, 2007.Google Scholar
  7. 7.
    J. Vidal, F. de Lamotte, G. Gogniat, P. Soulard and J.P. Diguet: “A Code-Design Approach for Embedded System Modeling and Code Generation with UML and MARTE”, proc. of the Design, Automation & Test in Europe Conference, DATE’09, IEEE, 2009.Google Scholar
  8. 8.
    IEEE: “Open SystemC Language Reference Manual”,
  9. 9.
    OSCI: “SystemC Users Group Survey Data Trends Report, April 2007”,
  10. 10.
    P. Coussy and A. Morawiec (Eds.): “High-level synthesis: from algorithm to digital circuit”, Springer, 2008.Google Scholar
  11. 11.
    A. Jantsch: “Modeling Embedded Systems and SoCs”, Morgan Kaufmann, 2004.Google Scholar
  12. 12.
    S. Bocchio, E. Riccobene, A. Rosti, P. Scandurra: “An Enhanced SystemC UML Profile for Modeling at Transaction-Level”, in E. Villar (ed.): “Embedded Systems Specification and Design Languages”, Springer, 2008.Google Scholar
  13. 13.
    P. Andersson and M. Höst.: “UML and SystemC a Comparison and Mapping Rules for Automatic Code Generation”, in E. Villar (ed.): “Embedded Systems Specification and Design Languages”, Springer, 2008.Google Scholar
  14. 14.
    J. Kreku, M. Hoppari and T. Kestilä: “SystemC workload model generation from UML for performance simulation”, in proc. of FDL’2007, ECSI, 2007.Google Scholar
  15. 15.
    E. Piel, R. B. Attitalah, P. Marquet, S. Meftali, S. Niar, A. Etien, J.L. Dekeyser, and P. Boulet: “Gaspard2: from MARTE to SystemC Simulation”, in proc. of Design, Automation and Test in Europe, DATE’2008, IEEE, 2008.Google Scholar
  16. 16.
    H. Störrle and J.H. Hausmann: “Towards a Formal Semantics of UML 2.0 Activities”, Software Engineering Vol. 64, 2005.Google Scholar
  17. 17.
    R. Eshuis and R. Wieringa: “A Formal Semantics for UML Activity Diagrams– Formalizing Workflow Models”, CTIT Technical Reports Series (01-04), 2001.Google Scholar
  18. 18.
    F. Mallet: “Clock constraint specification language: specifying clock constraints with UML/MARTE”, Innovations in Systems and Software Engineering, V.4, N.3, October, 2008).Google Scholar
  19. 19.
    D. Kroening and N. Sharygna: “Formal Verification of SystemC by Automatic Hardware/Software Partitioning”, in proc. of MEMOCODES’05, 2005.Google Scholar
  20. 20.
    F. Maraninchi, M. Moy and L. Maillet-Contoz: “Lussy: An Open Tool for the Analysis of Systems-on-a-Chip at the Transaction Level”, Design Automation of Embedded Systems, V.10, N.2-3, 2005.Google Scholar
  21. 21.
    C. Traulsem, J. Cornet, M. Moy and F. Maraninchi: “A SystemC/TLM semantics in PROMELA and its possible Applications”, in proc. of the Workshop on Model Checking Software, SPIN’2007, 2007.Google Scholar
  22. 22.
    J. Falk, C. Haubelt and J. Teich: “Efficient Representation and Simulation of Model-Based Designs in SystemC”, in proc. of FDL’2006, ECSI, 2006.Google Scholar
  23. 23.
    F. Herrera and E. Villar: “A framework for Embedded System Specification under Different Models of Computation in SystemC”, in proc. of the Design Automation Conference, DAC’2006, ACM, 2006.Google Scholar
  24. 24.
    W. Mueller, J. Ruf, D. Hoffmann, J. Gerlach, T. Kropf and W. Rosenstiel: “The Simulation Semantics of SystemC”, in proc. of Design, Automation and Test in Europe, DATE’2001, IEEE, 2001.Google Scholar
  25. 25.
    A. Salem: “Formal Semantics of Synchronous SystemC”, in proc. of Design, Automation and Test in Europe, DATE’2003, IEEE, 2003.Google Scholar
  26. 26.
    Ecker, W., Esen, V., Hull, M. Execution Semantics and Formalisms for Multi-Abstraction TLM Assertions. In Proc. of MEMOCODES’06. Napa, California. July, 2006.Google Scholar
  27. 27.
    M. Moy, F. Maraninchin and L. Maillet-Contoz: “SystemC/TLM Semantics for Heterogeneous System-on-Chip Validation”, in proc. of NEWCAS and TAISA Conference, IEEE, 2008.Google Scholar
  28. 28.
    E. Villar, F. Herrera and V. Fernández: “Formal support for Untimed SystemC Specifications: Application to high-level synthesis”, in proc. of FDL’2010, ECSI, 2010.Google Scholar
  29. 29.
    P. Peñil, H. Posadas and E. Villar: “Formal Modeling for UML-MARTE Concurrency Resources”, in proc. of the 15th Int. Conf. on Engineering of Complex Computer Systems, IEEE, 2010.Google Scholar
  30. 30.
    P. Peñil, J. Medina, H. Posadas and E. Villar: “Generating Heterogeneous Executable Specifications in SystemC from UML/MARTE Models”, in proc. of the 11th Int. Conference on Formal Engineering Methods, IEEE, 2009.Google Scholar
  31. 31.
    Raudvere, T, I. Sander and A. Jantsch: “Application and Verification of Local Non Semantic-Preserving Transformations in System Design”, IEEE Trans. on CAD of ICs and Systems, V.27, N.6, 2008.Google Scholar
  32. 32.
    Property Specification Language Ref. Manual. June, 2004.Google Scholar
  33. 33.
    Lee, E. A. and Sangiovanni-Vincentelli, A. 1998. A framework for comparing models of computation. IEEE Trans. Comput. Aided Des. Integrated Circ. Syst. 17, 12.Google Scholar

Copyright information

© Springer Science+Business Media, LLC 2012

Authors and Affiliations

  1. 1.E.T.S.I.I.T.University of CantabriaSantanderSpain

Personalised recommendations