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.
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.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
References
OMG: āMDA guide, Version 1.1ā, www.omg.org/mda, 2003.
B. Bailey, G. Martin and A. Piziali: āESL Design and Verificationā, Morgan Kaufman, 2007.
OMG: āUML 2.1 Superstructure Specificationā, www.uml.org, 2006.
L. Lavagno, G. Martin, B. Selic (Eds.): āUML for real: design of embedded real-time systemsā, Springer, 2003.
OMG: āUML Profile for MARTE, v1.0ā, www.omgmarte.org, 2009.
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.
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.
IEEE: āOpen SystemC Language Reference Manualā, http://standards.ieee.org/getieee/1666/download/1666-2005.pdf.
OSCI: āSystemC Users Group Survey Data Trends Report, April 2007ā, www.systemc.org/community/user_groups/OSCI_2007_Survey_Data_Trends_Report.pdf.
P. Coussy and A. Morawiec (Eds.): āHigh-level synthesis: from algorithm to digital circuitā, Springer, 2008.
A. Jantsch: āModeling Embedded Systems and SoCsā, Morgan Kaufmann, 2004.
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.
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.
J. Kreku, M. Hoppari and T. KestilƤ: āSystemC workload model generation from UML for performance simulationā, in proc. of FDLā2007, ECSI, 2007.
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.
H. Stƶrrle and J.H. Hausmann: āTowards a Formal Semantics of UML 2.0 Activitiesā, Software Engineering Vol. 64, 2005.
R. Eshuis and R. Wieringa: āA Formal Semantics for UML Activity Diagramsā Formalizing Workflow Modelsā, CTIT Technical Reports Series (01-04), 2001.
F. Mallet: āClock constraint specification language: specifying clock constraints with UML/MARTEā, Innovations in Systems and Software Engineering, V.4, N.3, October, 2008).
D. Kroening and N. Sharygna: āFormal Verification of SystemC by Automatic Hardware/Software Partitioningā, in proc. of MEMOCODESā05, 2005.
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.
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.
J. Falk, C. Haubelt and J. Teich: āEfficient Representation and Simulation of Model-Based Designs in SystemCā, in proc. of FDLā2006, ECSI, 2006.
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.
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.
A. Salem: āFormal Semantics of Synchronous SystemCā, in proc. of Design, Automation and Test in Europe, DATEā2003, IEEE, 2003.
Ecker, W., Esen, V., Hull, M. Execution Semantics and Formalisms for Multi-Abstraction TLM Assertions. In Proc. of MEMOCODESā06. Napa, California. July, 2006.
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.
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.
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.
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.
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.
Property Specification Language Ref. Manual. June, 2004.
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.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights 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)