Petri nets as supporting formalism within Embedded Systems Co-design

This paper presents a methodology for embedded systems hardware-software co-design, which main objective is to contribute to show Petri nets models adequacy to be used as the underlying formalism amenable to support specification, simulation, verification and implementation, including partitioning into components, co-simulation, co-verification and automatic code generation. The methodology starts grabbing user requirements through UML use-cases, which will be (manually) translated into behavioral sub-models, expressed in one of the following graphical formalisms: state diagrams, hierarchical and concurrent state diagrams, statecharts, sequence diagrams, and Petri nets. Those partial models will be translated into behaviorally equivalent Petri net models, which will be composed in order to obtain the overall system model amenable to support property verification and partitioning into components. For that end a set of (Petri) net operations are referred including net addition and net split. Integration of the tools under development and other common available tools is foreseen as PNML representation is used.