SysVeritas: A Framework for Verifying IOPT Nets and Execution Semantics within Embedded Systems Design

Abstract : We present a rewriting logic based technique for defining the formal executable semantics of a non-autonomous Petri net class, named Input-Output Place/Transition nets (IOPT nets), designed for model-based embedded system’s development, according to the MDA initiative. For this purpose, we provide model-to-model transformations from ecore IOPT models to a rewriting logic specification in Maude. The transformations are defined as semantic mappings based on the respective metamodels: the IOPT metamodel and the Maude metamodel. Also, we define model to-text transformations for the generation of the model execution code in the rewriting logic framework. Hence, we present a translational semantics composed by two components: (i) the denotational one, considering as semantic domains the operations, equations, and properties that specify the Petri net structure, signals, and events according to the commutative monoid view; and (ii) the operational one, that changes the interleaving semantics of Maude using rewriting rules specified at the Maude metalevel to provide a maximal step semantics for transitions with arcs, test arcs, and priorities. Additionally, this work gives architectural advices in order to compose new semantics specifications by simple component substitution. Due to its simulation and verification capabilities for control systems, the presented work was applied to a domotic project that intends to save energy in residential buildings.
Type de document :
Communication dans un congrès
Luis M. Camarinha-Matos. 2nd Doctoral Conference on Computing, Electrical and Industrial Systems (DoCEIS), Feb 2011, Costa de Caparica, Portugal. Springer, IFIP Advances in Information and Communication Technology, AICT-349, pp.256-265, 2011, Technological Innovation for Sustainability. 〈10.1007/978-3-642-19170-1_28〉
Liste complète des métadonnées

Littérature citée [10 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-01566552
Contributeur : Hal Ifip <>
Soumis le : vendredi 21 juillet 2017 - 11:25:16
Dernière modification le : vendredi 21 juillet 2017 - 11:34:17

Fichier

978-3-642-19170-1_28_Chapter.p...
Fichiers produits par l'(les) auteur(s)

Licence


Distributed under a Creative Commons Paternité 4.0 International License

Identifiants

Citation

Paulo Barbosa, João Barros, Franklin Ramalho, Luís Gomes, Jorge Figueiredo, et al.. SysVeritas: A Framework for Verifying IOPT Nets and Execution Semantics within Embedded Systems Design. Luis M. Camarinha-Matos. 2nd Doctoral Conference on Computing, Electrical and Industrial Systems (DoCEIS), Feb 2011, Costa de Caparica, Portugal. Springer, IFIP Advances in Information and Communication Technology, AICT-349, pp.256-265, 2011, Technological Innovation for Sustainability. 〈10.1007/978-3-642-19170-1_28〉. 〈hal-01566552〉

Partager

Métriques

Consultations de la notice

24

Téléchargements de fichiers

5