Generation of SystemC/TLM code from UML/MARTE sequence diagrams for verification

Verification of real time embedded systems at high level of abstraction is a challenging task that requires the simulation of the system and the checking of its timing and functional properties as well as constraints. The paper presents a methodology which starts from UML sequence diagrams with MARTE timing constraints and generates a SystemC/TLM model with checkers. The execution of the model allows to verify the specified sequence of exchanged information between components while checkers allow to verify that properties and timing constraints are met. The application of the methodology to the design of a wireless sensor node shows the validity of the approach and its simulation overhead.