Towards usage of formal methods within embedded systems co-design

This paper presents the planned and on-going activities inside the FORDESIGN research project, funded by the Portuguese FCT (Foundation for Science and Technology), whose main objective is to foster the effective use of formal methods for embedded systems co-design. The project proposes a methodology where the use-cases are used as a starting point, not only for capturing requirements but also to support sub-model compositions. The methodology will support several different graphical formalisms, namely state diagrams, hierarchical and concurrent state diagrams, state-charts, sequence diagrams, and Petri nets. The latter are also used as the interchange format between the other used graphical formalisms. Hence, translations to Petri nets play a fundamental role. These Petri nets are then implemented using hardware-software co-design techniques, which will include reconfigurable devices, as well as microcontroller architectures, as supporting platforms. The project also includes the definition of a generic mechanism for Petri nets composition. This will offer support for composition, hierarchical structuring, and model modification