Skip to main content
View expanded cover

System Specification and Design Languages pp 239–254Cite as

Formal Support for Untimed MARTE-SystemC Interoperability

  • 540 Accesses

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

Abstract

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.

Keywords

  • 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.

This work was financed by the ICT SATURN (FP7-216807) and COMPLEX (FP7-247999) European projects and by the Spanish MICyT project TEC 2008-04107.

This is a preview of subscription content, access via your institution.

Chapter
USD   29.95
Price excludes VAT (USA)
  • DOI: 10.1007/978-1-4614-1427-8_15
  • Chapter length: 16 pages
  • Instant PDF download
  • Readable on all devices
  • Own it forever
  • Exclusive offer for individuals only
  • Tax calculation will be finalised during checkout
eBook
USD   149.00
Price excludes VAT (USA)
  • ISBN: 978-1-4614-1427-8
  • Instant PDF download
  • Readable on all devices
  • Own it forever
  • Exclusive offer for individuals only
  • Tax calculation will be finalised during checkout
Softcover Book
USD   189.00
Price excludes VAT (USA)
Hardcover Book
USD   199.99
Price excludes VAT (USA)
Learn about institutional subscriptions
Fig. 15.1
Fig. 15.2
Fig. 15.3
Fig. 15.4
Fig. 15.5

References

  1. OMG: “MDA guide, Version 1.1”, www.omg.org/mda, 2003.

  2. B. Bailey, G. Martin and A. Piziali: “ESL Design and Verification”, Morgan Kaufman, 2007.

    Google Scholar 

  3. OMG: “UML 2.1 Superstructure Specification”, www.uml.org, 2006.

  4. L. Lavagno, G. Martin, B. Selic (Eds.): “UML for real: design of embedded real-time systems”, Springer, 2003.

    Google Scholar 

  5. OMG: “UML Profile for MARTE, v1.0”, www.omgmarte.org, 2009.

  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. 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. IEEE: “Open SystemC Language Reference Manual”, http://standards.ieee.org/getieee/1666/download/1666-2005.pdf.

  9. OSCI: “SystemC Users Group Survey Data Trends Report, April 2007”, www.systemc.org/community/user_groups/OSCI_2007_Survey_Data_Trends_Report.pdf.

  10. P. Coussy and A. Morawiec (Eds.): “High-level synthesis: from algorithm to digital circuit”, Springer, 2008.

    Google Scholar 

  11. A. Jantsch: “Modeling Embedded Systems and SoCs”, Morgan Kaufmann, 2004.

    Google Scholar 

  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. 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. 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. 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. H. Störrle and J.H. Hausmann: “Towards a Formal Semantics of UML 2.0 Activities”, Software Engineering Vol. 64, 2005.

    Google Scholar 

  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. 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. D. Kroening and N. Sharygna: “Formal Verification of SystemC by Automatic Hardware/Software Partitioning”, in proc. of MEMOCODES’05, 2005.

    Google Scholar 

  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. 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. 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. 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. 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. A. Salem: “Formal Semantics of Synchronous SystemC”, in proc. of Design, Automation and Test in Europe, DATE’2003, IEEE, 2003.

    Google Scholar 

  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. 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. 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. 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. 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. 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. Property Specification Language Ref. Manual. June, 2004.

    Google Scholar 

  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 

Download references

Author information

Authors and Affiliations

  1. E.T.S.I.I.T., University of Cantabria, TEISA Dpt. Av. Los Castros s/n, Santander, Spain

    Pablo Peñil, Fernando Herrera & Eugenio Villar

Authors
  1. Pablo Peñil
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Fernando Herrera
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Eugenio Villar
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Pablo Peñil .

Editor information

Editors and Affiliations

  1. University of Southampton, Southampton, United Kingdom

    Tom J. Kaźmierski

  2. ECSI, Gières, France

    Adam Morawiec

Rights and permissions

Reprints and Permissions

Copyright information

© 2012 Springer Science+Business Media, LLC

About this paper

Cite this paper

Peñil, P., Herrera, F., Villar, E. (2012). Formal Support for Untimed MARTE-SystemC Interoperability. In: Kaźmierski, T., Morawiec, A. (eds) System Specification and Design Languages. Lecture Notes in Electrical Engineering, vol 106. Springer, New York, NY. https://doi.org/10.1007/978-1-4614-1427-8_15

Download citation

  • DOI: https://doi.org/10.1007/978-1-4614-1427-8_15

  • Published:

  • Publisher Name: Springer, New York, NY

  • Print ISBN: 978-1-4614-1426-1

  • Online ISBN: 978-1-4614-1427-8

  • eBook Packages: EngineeringEngineering (R0)