MDA-Based Methodology for Verifying Distributed Executionof Embedded Systems Models

Model-based development for embedded system design has been used to accommodate the increase insystem's complexity. Several modeling formalisms proved to be well matched for usage within this area.The goal of this chapter is to present a model-based development methodology for embedded systemsdesign. One of the main aims of this methodology is to contribute for usage of Petri nets as a systemspecification language within model-based development of embedded systems integrating MDA (Model-Driven Architecture) proposals as a reference for the development flow. Distributed execution of theinitial developed platform-independent models is achieved through model partitioning into platformspecificsub-modules. System model decomposition is obtained through a net splitting operation. Twotypes of implementation platforms are considered: compliant and non-compliant with zero time delayfor communication between modules (in other words, compliant or not with synchronous paradigm).Using a model-checking framework, properties associated to the execution of the distributed models inboth types of platforms are compared with the execution of the initial model.