Petri Net Based Model-Driven Design Of Embedded Softwares

As embedded devices gain much more computation power nowadays,embedded software can complete much more complex tasks.To complete a complex task usually involves the interaction of multiple components.In the traditional development approach of embedded software,the correctness of interactions between components can only be verified in the later phases of development via the system integration test.However,design defects found in later phases will lead to very high repair cost.In this paper,we propose the computation model Interactive Petri nets based on the Petri nets computation model and the supporting toolkit Tsmart-IPNEX to address the challenge of modeling the interaction of heterogeneous components in the model-driven design approach of embedded software.1)We propose the computation model Interactive Petri nets which feature modeling the interaction between components in embedded software.We define the syntax and semantics of Interaction Petri nets by extending Petri nets with modeling primitives for the composition of components.Interactive Petri nets offer the component composition mechanism to support the workflow which each sub-component is modeled independently and the interaction of sub-components and the scheduler component is defined to get an integrated system model,such that the modeled system and the model show the consistency in both behavior and structure.Interactive Petri nets offer rich data types similar to Coloured Petri nets.Dislike the functional language based on the standard ML for data type extension in Coloured Petri nets,Interactive Petri nets use a subset of C language to express user-defined types and functions,which is more suitable for the development of embedded software in the industry.2)We develop the integrated toolkit Tsmart-IPNEXto support the graphical model editing,simulation,verification and code synthesis of Interactive Petri nets models.Tsmart-IPNEXtoolkit implements a graphical model editor for Interactive Petri nets based on the Eclipse Graphical Modelling Framework,which is more intuitive than a text model editor.Tsmart-IPNEXtoolkit implements an interactive model simulator,in which users can perform step-forward,backward and reset operations to traverse the state-space of models.Tsmart-IPNEXtoolkit supports the verification of Interactive Petri nets models by transforming the models to the input form of the VCS model-checking tool.Tsmart-IPNEXtoolkit implements the code synthesis function which transforms the Interactive Petri nets model to C programs on particular platforms.Overall,Tsmart-IPNEXtoolkit implements many features to support the model-driven design of embedded software,which facilitates the implementation of embedded software.