Reference Hub2
MDA-Based Methodology for Verifying Distributed Execution of Embedded Systems Models

MDA-Based Methodology for Verifying Distributed Execution of Embedded Systems Models

Anikó Costa (Universidade Nova de Lisboa, Portugal), Paulo E. S. Barbosa (Universidade Estadual da Paraiba, Brazil), Filipe Moutinho (Universidade Nova de Lisboa, Portugal), Fernando Pereira (Instituto Politécnico de Lisboa, Portugal), Franklin Ramalho (Universidade Federal de Campina Grande, Brazil), Jorge C. A. Figueiredo (Universidade Federal de Campina Grande, Brazil) and Luis Gomes (Universidade Nova de Lisboa, Portugal)
Copyright: © 2013 |Pages: 24
ISBN13: 9781466640344|ISBN10: 1466640340|EISBN13: 9781466640351|ISSN: 2326-6139|EISSN: 2326-6155
DOI: 10.4018/978-1-4666-4034-4.ch006
Cite Chapter Cite Chapter

MLA

Costa, Anikó, Paulo E. S. Barbosa, Filipe Moutinho, Fernando Pereira, Franklin Ramalho, Jorge C. A. Figueiredo and Luis Gomes. "MDA-Based Methodology for Verifying Distributed Execution of Embedded Systems Models." Formal Methods in Manufacturing Systems: Recent Advances. IGI Global, 2013. 112-135. Web. 27 Mar. 2020. doi:10.4018/978-1-4666-4034-4.ch006

APA

Costa, A., Barbosa, P. E., Moutinho, F., Pereira, F., Ramalho, F., Figueiredo, J. C., & Gomes, L. (2013). MDA-Based Methodology for Verifying Distributed Execution of Embedded Systems Models. In Z. Li, & A. Al-Ahmari (Eds.), Formal Methods in Manufacturing Systems: Recent Advances (pp. 112-135). Hershey, PA: IGI Global. doi:10.4018/978-1-4666-4034-4.ch006

Chicago

Costa, Anikó, Paulo E. S. Barbosa, Filipe Moutinho, Fernando Pereira, Franklin Ramalho, Jorge C. A. Figueiredo and Luis Gomes. "MDA-Based Methodology for Verifying Distributed Execution of Embedded Systems Models." In Formal Methods in Manufacturing Systems: Recent Advances, ed. Zhiwu Li and Abdulrahman M. Al-Ahmari, 112-135 (2013), accessed March 27, 2020. doi:10.4018/978-1-4666-4034-4.ch006

Export Reference

Mendeley
Favorite

Abstract

Model-based development for embedded system design has been used to accommodate the increase in system’s complexity. Several modeling formalisms proved to be well matched for usage within this area. The goal of this chapter is to present a model-based development methodology for embedded systems design. One of the main aims of this methodology is to contribute for usage of Petri nets as a system specification language within model-based development of embedded systems integrating MDA (Model-Driven Architecture) proposals as a reference for the development flow. Distributed execution of the initial developed platform-independent models is achieved through model partitioning into platform-specific sub-modules. System model decomposition is obtained through a net splitting operation. Two types of implementation platforms are considered: compliant and non-compliant with zero time delay for communication between modules (in other words, compliant or not with synchronous paradigm). Using a model-checking framework, properties associated to the execution of the distributed models in both types of platforms are compared with the execution of the initial model.

References

W3C Recommendation. (2010). XQuery 1.0 and XPath 2.0 formal semantics, second ed., 14 December 2010. Retrieved from http://www.w3.org/TR/xquery-semantics/
W3C Recommendation. (2011). Scalable vector graphics (SVG) 1.1, second ed., 16 August 2011. Retrieved from http://www.w3.org/TR/SVG/
Barbosa P. Ramalho F. Figueiredo J. Junior A. Costa A. Gomes L. (2009). Checking semantics equivalence of mda transformations in concurrent systems.Journal of Universal Computer Science, 15(11), 2196–2224.
Barros, J., & Gomes, L. (June 2004). Net model composition and modification by net operations: a pragmatic approach. In Proceedings of the 2nd IEEE International Conference on Industrial Informatics (INDIN 2004). IEEE.
Bezivin, J., Breton, E., Valduriez, P., & Dupr, G. (2003). The ATL transformation-based model management framework. Retrieved from http://www.lina.sciences.univnantes.fr/Publications/2003/JBVD03
Billington, J., Christensen, S., van Hee, K., Kindler, E., Kummer, O., & Petrucci, L. … Weber, M. (2003). The petri net markup language: Concepts, technology, and tools. In Proceedings of the 24th International Conference on Application and Theory of Petri Nets 2003 (LNCS), (vol. 2679, pp. 483-505). Berlin: Springer.
Breton, E., & Bézivin, J. (2001). Towards an understanding of model executability. In Proceedings of the International Conference on Formal Ontology in Information Systems. New York, NY: ACM.
Christensen S. Hansen N. D. (1992). Coloured petri nets extended with channels for synchronous communication.Lecture Notes in Computer Science, 815, 159–178. 10.1007/3-540-58152-9_10
Costa, A., Barbosa, P., Gomes, L., Ramalho, F., Figueiredo, J., & Junior, A. (2010). Properties preservation in distributed execution of petri nets models. In Emerging Trends in Technological Innovation IFIP Advances in Information and Communication Technology. DOI: 10.1007/978-3-642-11628-5_26
Costa, A., & Gomes, L. (2009). Petri net partitioning using net splitting operation. In Proceedings of INDIN. IEEE.
Edmund J. Clarke M. Grumberg O. Peled D. A. (1999). Model checking. Cambridge, MA: MIT Press.
Emerson E. A. Clarke E. M. (1982). Using branching time temporal logic to synthesize synchronization skeletons.Science of Computer Programming, 2(3), 241–266. 10.1016/0167-6423(83)90017-5
Gajski D. D. Abdi S. Gerstlauer A. Sshirner G. (2009). Embedded system design modeling. In Syntehesis and Verification. Berlin: Springer.
Gargantini P. S. A. Riccobene E. (2009). Model-driven design and ASM validation of embedded systems. In Behavioral Modeling for Embedded Systems and Technologies. Hershey, PA: IGI. 10.4018/978-1-60566-750-8.ch002
Girault C. Valk R. (2003). Petri nets for systems engineering. Academic Press. 10.1007/978-3-662-05324-9
Gomes L. Barros J. P. (2005). Structuring and composability issues in petri nets modeling.IEEE Transactions on Industrial Informatics, 1(2), 112–123. 10.1109/TII.2005.844433
Gomes, L., Barros, J. P., Costa, A., & Nunes, R. (2007). The input-output place-transition Petri net class and associated tools. In Proceedings of the 5th IEEE International Conference on Industrial Informatics. IEEE.
Gomes L. Barros J. P. Costa A. Pais R. Moutinho F. (2005). Formal methods for embedded systems co-design: The FORDESIGN project, ReCoSoC’05 - Reconfigurable communication-centric systems-on-chip. Academic Press.
Gomes, L., Barros, J. P., Costa, A., Pais, R., & Moutinho, F. (2005). Towards usage of formal methods within embedded systems co-design. Paper presented at the ETFA’2005 - 10th International Conference on Emergent Technologies and Factory Automation. Catania, Italy.
Gomes L. Fernandes J. M. (2009). Behavioral modeling for embedded systems and technologies. Hershey, PA: IGI. 10.4018/978-1-60566-750-8
Lisane L. C. de Brisolara B. Kreutz M. E. (2009). UML as front-end language for embedded systems design. In Behavioral Modeling for Embedded Systems and Technologies. Hershey, PA: IGI.
Miller J. Mukerji J. (2003). Mda guide version 1.0.1. Object Management Group. OMG.
Moutinho, F., Gomes, L., Ramalho, F., Figueiredo, J., Barros, J. P., Barbosa, P., et al. (2010). ecore representation for extending PNML for input-output place-transition nets. In Proceedings of 36th Annual Conference of the IEEE Industrial Electronics Society. Phoeniz, AZ: IEEE.
Murata T. (1989). Petri nets: Properties, analysis and applications.Proceedings of the IEEE, 77(4), 541–580. 10.1109/5.24143
OMG. (2008). Object management group. Retrieved from http://www.omg.org
Pereira, F., Moutinho, F., & Gomes, L. (2012). Model-checking framework for embedded systems controllers development using IOPT petri nets. In Proceedings of the ISIE’2012 – 21th IEEE International Symposium on Industrial Electronics. Hangzhou, China: IEEE.
Pereira, F., Moutinho, F., Gomes, L., & Campos-Rebelo, R. (2012). IOPT petri net state space generation algorithm with maximal-step execution semantics. In Proceedings of INDIN’2011 - 9th IEEE International Conference on Industrial Informatics, (pp. 789 - 795). DOI 10.1109/INDIN.2011.6034958
Pereira, F., Moutinho, F., Ribeiro, J., & Gomes, L. (2012). Web based IOPT petri net editor with an extensible plug-in architecture to support generic net operations. In Proceedings of the IECON’2012 – The 38th Annual Conference of the IEEE Industrial Electronics Society. Montreal, Canada: IEEE.
Reisig W. (1985). Petri nets: An introduction. New York: Springer-Verlag.
Ribeiro, J., Moutinho, F., Pereira, F., & Gomes, L. (2011). An ecore based petri net type definition for PNML IOPT models. In Proceedings of INDIN’2011 – 9th IEEE International Conference on Industrial Informatics. Lisbon, Portugal: IEEE.
Ribeiro, O. R., Fernandes, J. M., & Pinto, L. F. (2005). Model checking embedded systems with PROMELA. In Proceedings of the 12th IEEE International Conference and Workshops on Engineering of Computer-Based Systems. Washington, DC: IEEE Computer Society.
Salewski F. Kowalewski S. (2008). Hardware/software design considerations for automotive embedded systems.IEEE Transactions on Industrial Informatics, 4(3), 156–163. 10.1109/TII.2008.2002919
Sasa A. Juric M. B. Krisper M. (2008). Service-oriented framework for human task support and automation.IEEE Transactions Industrial Informatics, 4(4), 292–302. 10.1109/TII.2008.2008641
Silva M. (1985). Las redes de petri: En la automática y la informática. Madrid: Editorial AC.

Request Access

You do not own this content. Please login to recommend this title to your institution's librarian or purchase it from the IGI Global bookstore.