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.
Chapter PDF
Similar content being viewed by others
References
Gomes, L., Fernandes, J.M.: Behavioral Modeling for Embedded Systems and Technologies. Information Science Reference (2009)
Sgroi, M., Lavagno, L., Sangiovanni-Vincentelli, A.: Formal models for embedded system design. IEEE Des. Test 17, 14–27 (2000)
Gomes, L., Barros, J.P., Costa, A., Pais, R., Moutinho, F.: Formal Methods for Embedded Systems Co design: the FORDESIGN Project. In: Proceedings of Workshop Reconfigurable Communication-centric Systems-on Chip, ReCoSoC 2005 (2005)
Girault, C., Rüdiger, V.: Petri Nets for Systems Engineering. In: XV, Hardcover, p. 607 (2003)
Barbosa, P., Costa, A., Ramalho, F., Figueiredo, J., Gomes, L., Junior, A.: Checking Semantics Equivalence of MDA Transformations in Concurrent Systems. Journal of Universal Computer Science (J.UCS) (to appear 2009), http://www.jucs.org/jucs
OMG: Model-Driven Architecture (2008), http://www.omg.org/mda/
Barbosa, P., Ramalho, F., Figueiredo, J., Costa, A., Gomes, L., Junior, A.: Semantic equations for formal models in the model-driven architecture. In: Camarinha-Matos, L.M., Pereira, P., Ribeiro, L. (eds.) DoCEIS 2010. IFIP Advances in Information and Communication Technology, vol. 314, pp. 251–260. Springer, Heidelberg (2010)
Moutinho, F., Gomes, L., Ramalho, F., Figueiredo, J., Barros, J.P., Barbosa, P., Pais, R., Costa, A.: Ecore Representation for Extending PNML for Input-Output Place-Transition Nets. In: 36th Annual Conference of the IEEE Industrial Electronics Society, IECON 2010, Glendale, AZ, November 7-10 (2010)
Ellson, J., Gansner, E., Koutsofios, L., North, S., Woodhull, G., Description, S., Technologies, L.: Graphviz. In: Open Source Graph Drawing Tools. LNCS, pp. 483–484. Springer, Heidelberg (2001)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2011 IFIP International Federation for Information Processing
About this paper
Cite this paper
Barbosa, P. et al. (2011). SysVeritas: A Framework for Verifying IOPT Nets and Execution Semantics within Embedded Systems Design. In: Camarinha-Matos, L.M. (eds) Technological Innovation for Sustainability. DoCEIS 2011. IFIP Advances in Information and Communication Technology, vol 349. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-19170-1_28
Download citation
DOI: https://doi.org/10.1007/978-3-642-19170-1_28
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-19169-5
Online ISBN: 978-3-642-19170-1
eBook Packages: Computer ScienceComputer Science (R0)