Article Preview
Top1. Introduction
Embedded systems are becoming pervasive in our everyday life. These systems have many applications including automotive and aircraft controllers, cellular phones, network switches, household appliances, medical devices, and consumer electronics.
An embedded system can be defined as a computer that is a component in a large system and that relies on its own microprocessor. Thus, it can be viewed as a mix of cooperating hardware and software parts, which are able to provide a wider and more adaptable set of complex functionalities without requiring a large amount of resources needed by general purpose systems (Mokhati, Gagnon & Badri, 2008). Embedded systems typically have an intensive real-time interaction with their environment. In those systems, the correct behavior depends not only on the integrity of the results, but also on the time the results are produced. Since such systems are particularly suited in real-time contexts, where tasks must be performed within a given deadline, predictability (determinism) can become a key issue.
The design of an embedded system is a very challenging task which involves the cooperation of different experts (Mirko, Tiziana, Graziano, & Bernhard, 2005). The modern approach of design introduces the concept of model with a well-defined semantics so that the different tasks from specification to implementation can systematically be carried out.
UML (Unified Modeling Language) is a language for specifying, visualizing and constructing the artifacts of software systems (Rumbaugh, Booch & Jacobson, 1999). UML started also to be used for modeling real-time and embedded software systems (DámDarvas, Majzik & Benyó, 2002). It offers the description of several views of a system. It consists of many diagrams. Some diagrams are used to model the structure of a system while others are used to model the behavior of a system. UML Statechart diagram models the lifetime (states life cycle) of an object in response to events (Heral, 1987). A UML collaboration diagram models the interaction between a set of objects through the messages (or events) that may be dispatched among them. Real-Time Statecharts, and Real-Time Collaboration diagrams which can efficiently specify explicit dense time, are an extension of the precedent diagrams with real-time constructs (Kesteney & Pnueli, 2005).
However, despite UML’s success as being a unified and visual notation in software engineering field, UML suffers from a lack of formal semantics. This leads to inconsistencies and errors in the developed models that are hard to find manually (or even impossible in the case of complex systems) (DámDarvas, Majzik & Benyó, 2002). As a subset of UML is extended with timing annotations and given a formal semantics, UML diagrams can be translated, via ATOM3 (A Tool for Multi-formalism and Meta-Modeling) to the input format of model-checking; to be formally verified.
The rewriting logic of Maude is considered as one of the most powerful languages in the specification and verification of concurrent systems (McCombs, 2003). Maude Model checker is included with the Maude environment; it attempts to validate the behavior of a system using different properties described using a given logic (LTL, CTL) (Gagnon. 2007).
In this context, one of the possible approaches consists in deriving automatically formal specifications (Maude in our case) from UML models and analyzing them formally. An object-based development process begins by the generation of visual modeling tool based on two behaviors of UML diagrams (Real-Time Statechart and Real-Time Collaboration). Then, from the resulting models, Maude specifications will be generated and verified by a Maude model checker.
Building a modeling tool from the scratch is a prohibitive task. A meta-modeling approach is useful to deal with this problem (DeLara & Guerra, 2003). In meta-modeling, formalisms are described at a meta-level. This information is used by a meta-model processor to generate modeling tools for the described formalisms.
Meta-modeling can be combined with graph grammars to extend the model manipulation capabilities of the generated modeling tools: edit, simulate, transform into formalism, optimize and generate code (DeLara & Vangheluwe, 2004). In our approach we apply graph grammar to have last kind of model transformation. These ideas presented above are implemented in ATOM3 (DeLara & Vangheluwe, 2002).