Cross modeling of embedded systems using SysML and Petri Nets

Cross modeling in embedded systems development is proposed in the paper. The main idea consists in a translation of SysML artifacts into the related Coloured Petri Net (CPN) models, which may be verified directly or using other tools, e.g. Temporal Logic Provers. The paper is an extension of [20] mainly by insertion of sequence diagrams (SysML) and presentation of their mapping into CPN models. The additional part describes communication features and completes the cross modeling approach