{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,28]],"date-time":"2025-11-28T17:21:21Z","timestamp":1764350481732},"reference-count":28,"publisher":"IGI Global","issue":"2","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2018,7]]},"abstract":"<jats:p>The approach proposed in this article presents a formal verification of embedded systems. The method relies on an automated modeling and code generation based on the systems' behavior. The key concept is the combined use of a subset of UML behavior diagrams extended with timing annotations (Real-Time Statechart and Real-Time Collaboration diagrams) for system modeling and the Maude language for verification. First, UML modeling tools are developed. Then, an automatic generation of equivalent Maude specification is performed. The approach is based on code generation. This is why it is possible to use an available model checking tool to verify certain timed properties represented in Linear Temporal Logic (LTL). The meta-modeling tool ATOM3 is used. A case study is presented to illustrate the feasibility of the approach.<\/jats:p>","DOI":"10.4018\/ijcssa.2018070103","type":"journal-article","created":{"date-parts":[[2019,7,10]],"date-time":"2019-07-10T16:19:20Z","timestamp":1562775560000},"page":"42-58","source":"Crossref","is-referenced-by-count":1,"title":["Embedded System Verification Using Formal Model an Approach Based on the Combined Use of UML and Maude Language"],"prefix":"10.4018","volume":"6","author":[{"given":"Meliouh","family":"Amel","sequence":"first","affiliation":[{"name":"University of Msila, Msila, Algeria"}]},{"given":"Chaoui","family":"Allaoua","sequence":"additional","affiliation":[{"name":"University of Constantine 2, Constantine, Algeria"}]}],"member":"2432","reference":[{"key":"IJCSSA.2018070103-0","unstructured":"AGG Home page. (n.d.). Retrieved from http:\/\/tfs.cs.tu-berlin.de\/agg\/"},{"key":"IJCSSA.2018070103-1","unstructured":"ATOM3 Home page. (n.d.). Retrieved from http:\/\/atom3.cs.mcgill.ca\/"},{"key":"IJCSSA.2018070103-2","author":"G.Booch","year":"2005","journal-title":"The unified modeling language user guide"},{"key":"IJCSSA.2018070103-3","doi-asserted-by":"crossref","unstructured":"Bourahla, M. (2009). Modeling and Verification of Real-Time Embedded Systems, the third international conference on Innovation and Information and Communication Technology, Amman, Jordan.","DOI":"10.14236\/ewic\/ISIICT2009.6"},{"key":"IJCSSA.2018070103-4","doi-asserted-by":"crossref","unstructured":"Boutekkouk, B.F. (2009). UML Modeling and Formal Verification of control\/data driven Embedded Systems, UML AADL Workshop Potsdam, Germany.","DOI":"10.1109\/ICECCS.2009.30"},{"key":"IJCSSA.2018070103-5","unstructured":"Cabodi, G., Camurati, P., Loiacono, C., Pipitone, G., Savarese, F., & Vendraminetto, D. (2015). Formal Verification of Embedded Systems for Remote Attestation. WSEAS Transactions On Computers, 14."},{"key":"IJCSSA.2018070103-6","first-page":"511","article-title":"A Graph Transformation Approach to Generate Analysable Maude Specifications from UML Interaction Overview Diagrams","author":"D.Chafika","year":"2018","journal-title":"IEEE International Conference on Information Reuse and Integration"},{"key":"IJCSSA.2018070103-7","unstructured":"D\u00e1mDarvas. I., Majzik, A., & Beny\u00f3,B. (2002). Verification of statechart UML models of Embedded sytems. University of Technology and Economics, Dept. of Measurement and Information Systems."},{"key":"IJCSSA.2018070103-8","doi-asserted-by":"publisher","DOI":"10.1016\/j.jvlc.2004.01.005"},{"key":"IJCSSA.2018070103-9","doi-asserted-by":"publisher","DOI":"10.1007\/s10270-003-0047-5"},{"key":"IJCSSA.2018070103-10","first-page":"12","author":"J.DeLara","year":"2003","journal-title":"Towards the Uniform Manipulation of Visual and Textual Languages in ATOM3. Prole\u201903: III Jornadas de Programaci\u00f3n y Lenguajes"},{"key":"IJCSSA.2018070103-11","doi-asserted-by":"crossref","unstructured":"DeLara, J., & Vangheluwe, H. (2002). ATOM3: A Tool for Multi-Formalism Modelling and Meta-Modelling. In FASE '02 Proceedings of the 5th International Conference on Fundamental Approaches to Software Engineering (pp. 174-188). Academic Press.","DOI":"10.1007\/3-540-45923-5_12"},{"key":"IJCSSA.2018070103-12","unstructured":"Francisco, A, M., Marcio, F., & Flavio, R. (2009). Using MDE for the Formal Verification of Embedded Systems Modeled by UML Sequence Diagrams. Institute of Informatics - Federal University of Rio Grande do Sul \u2013 UFRGS."},{"key":"IJCSSA.2018070103-13","author":"P.Gagnon","year":"2007","journal-title":"Verification Formelle de Diagrammes UML: Une Approche Bas\u00e9e sur la Logique de R\u00e9\u00e9criture, M\u00e9moire de maitrise en math\u00e9matiques et informatique appliqu\u00e9es"},{"key":"IJCSSA.2018070103-14","doi-asserted-by":"crossref","unstructured":"Heral, D., (1987). Statechart: A Visual Formalism for Complex Systems. Science of Computer Programming. Science ofComputer Programmingarchive, 8(3), 231-274.","DOI":"10.1016\/0167-6423(87)90035-9"},{"key":"IJCSSA.2018070103-15","first-page":"261","article-title":"Model Checking for Timed Statecharts.","author":"Q.Junyan","year":"2005","journal-title":"IFIP International Federation for Information Processing"},{"key":"IJCSSA.2018070103-16","doi-asserted-by":"crossref","first-page":"591","DOI":"10.1007\/3-540-55092-5_32","article-title":"Timed and hybrid statecharts and their textual representation.","author":"Y.Kesten","year":"1992","journal-title":"International Symposium on Formal Techniques in Real-Time and Fault-Tolerant Systems"},{"key":"IJCSSA.2018070103-17","unstructured":"Luis, A. C. (2005). A Petri Net based Modeling and Verification Technique for Real-Time Embedded Systems. Link\u00f6pings university, Sweden."},{"key":"IJCSSA.2018070103-18","unstructured":"McCombs, T. (2003). Maude 2.0 Primer, Version 1.0."},{"key":"IJCSSA.2018070103-19","author":"J.Meseguer","year":"2003","journal-title":"Software Specification and Verification in Rewriting Logic, Unpublished work"},{"issue":"6","key":"IJCSSA.2018070103-20","article-title":"Dynamic and formal verification of Embedded Systems: A Comparative Survey.","volume":"33","author":"L.Mirko","year":"2005","journal-title":"International Journal of Parallel Programming"},{"key":"IJCSSA.2018070103-21","doi-asserted-by":"publisher","DOI":"10.5381\/jot.2008.7.1.a1"},{"key":"IJCSSA.2018070103-22","unstructured":"Raphael, M. (2008). Modeling and Verifying Embedded Operating Systems [master thesis]. Swiss federal institute of technology, Zurich."},{"key":"IJCSSA.2018070103-23","unstructured":"Said, M., Allaoua, C., Martin, S., & Elhillali, K, (2018). Verification of Model Transformations Using Isabelle\/HOL and Scala. Information Systems Frontiers Journal."},{"key":"IJCSSA.2018070103-24","author":"B.Sven","year":"1999","journal-title":"The Fujaba RealTime Statechart PlugIn, course of the Special Research Initiative 614 - Self-optimizing Concepts and Structures in Mechanical Engineering"},{"key":"IJCSSA.2018070103-25","unstructured":"TGG Home page. (n.d.). Retrieved from http:\/\/cs.uni-paderborn.de\/404-fehlerseite"},{"key":"IJCSSA.2018070103-26","unstructured":"Vassil, T., Fr\u00e9d\u00e9ric, B., & Safouan, T. (2018). Formal verification of automotive embedded software. In FORMALISE:6th International Conference on Formal Methods in Software Engineering, Gothenburg, Sweden. Academic Press."},{"key":"IJCSSA.2018070103-27","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-40985-6_6"}],"container-title":["International Journal of Conceptual Structures and Smart Applications"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.igi-global.com\/viewtitle.aspx?TitleId=233534","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,5,5]],"date-time":"2022-05-05T22:17:52Z","timestamp":1651789072000},"score":1,"resource":{"primary":{"URL":"http:\/\/services.igi-global.com\/resolvedoi\/resolve.aspx?doi=10.4018\/IJCSSA.2018070103"}},"subtitle":[""],"short-title":[],"issued":{"date-parts":[[2018,7]]},"references-count":28,"journal-issue":{"issue":"2"},"URL":"https:\/\/doi.org\/10.4018\/ijcssa.2018070103","relation":{},"ISSN":["2166-7292","2166-7306"],"issn-type":[{"value":"2166-7292","type":"print"},{"value":"2166-7306","type":"electronic"}],"subject":[],"published":{"date-parts":[[2018,7]]}}}