Formal Modeling for UML/MARTE Concurrency Resources

Nowadays, complexity of embedded systems is increasing. This increasing complexity is due to the behavioural heterogeneity and the variety in the nature of system components. Additionally, it is essential to deal with the massive concurrency of such components. Therefore, as a consequence of these critical system aspects, the modelling of current embedded systems has become a challenge for the designers. In order to address this challenge, the UML/MARTE profile has been created. The MARTE profile provides the essential capabilities to develop design methodologies able to cover most of the main design steps. However, to understand and later to model current complex embedded systems in a univocal, well-defined way, formal foundations are required. This paper introduces a formal framework able to support methodologies that tackle the design of current embedded systems using the MARTE profile. In this paper the Generic Resource Modelling (GRM) subprofile of MARTE is used. The required formal foundations are provided by the Formal System Design (ForSyDe) formalism. This paper defines an abstraction methodology able to generate the corresponding ForSyDe model from the MARTE concurrency resources.