MDA-Based Methodology for Verifying Distributed Execution of Embedded Systems Models

Introduction

The sustained growing of available resources at chip level permits to have more and more complex systems implemented in one chip. These improvements lead us to have embedded systems everywhere and bring up embedded system design as an important research area. However, due to the lack of adequate methods and tools, this expansion has not been balanced with identical increase at the designer productivity. The adoption of a model-based development approach can adequately support improvements in current system's development flow, as stated in some recent publications in this area, such as (Gomes & Fernandes 2009) and (Gajski, Abdi, Gerstlauer & Sshirner 2009).

Usually, embedded systems are composed by software and hardware components. As an intrinsic requirement for this fact, starting with a global system model, it is necessary to decompose it into several sub-models. Furthermore, each sub-model is able to represent a component of the system.

In order to reduce time to market, it is necessary finding or developing adequate methods and formalisms supporting embedded system design. These formalisms should combine an understandable format for representing concepts supported by a powerful computational tools set plus analysis methods. Petri nets (Reisig 1985), (Girault & Valk 2003) can be seen as a system specification language satisfying these goals and contributing to the improvement of the development process. Petri nets are widely acknowledged as adequate for modeling concurrency, parallelism and synchronization of processes. These characteristics are present in most common applications for the embedded systems field. In addition, Petri nets can bring a sound semantics and strong support for verification of system properties, which is a key aspect as much as system complexity increases.

On the other hand, still considering the embedded systems design area, it is common to deal with large Petri nets models, namely in terms of the components that constitute a net. Moreover, it is very common to have the need to cope with specific constraints, namely to be compliant with specific real-time dependencies and to accommodate specific power consumption and/or cost requirements. In these situations, one must need to face the decomposition of the system model into a set of concurrent sub-models, which will be executed as concurrent components. Those components can potentially have different requirements in terms of performance and real-time response and be deployed into heterogeneous platforms, supporting an easier finding of balanced solutions considering specific requirements in terms of cost/performance ratio. This is also the case whenever distributed execution of the Petri net model is necessary, and is also closely related with hardware-software embedded systems co-design, where is needed to assure the deployment of the partitioned system model into components and into software and/or hardware implementation platforms or into multi-processor architectures. For this purpose, the net splitting operation (Costa & Gomes 2009) was introduced to allow the partitioning of a Petri net model into several sub-models, which can be executed concurrently, and support the referred goals.

As common whenever is necessary partitioning the model into several sub-models, it is necessary to introduce communication between those sub-models. By introducing communication between components within distributed execution supported by heterogeneous platforms, concurrent characteristics associated with the obtained sub-models may, potentially, impose some changes in some critical properties associated with the original model. By using model-checking (Edmund, Clarke, Grumberg & Peled 1999) techniques we can conclude whether the execution of the original model and the parallel execution of those transformed models behave properly or not (from a selected set of properties point of view).

Several approaches can be followed to allow model execution, in-line with the above mentioned goals, namely: