{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,5,6]],"date-time":"2022-05-06T10:12:36Z","timestamp":1651831956781},"reference-count":30,"publisher":"IGI Global","issue":"4","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2017,10]]},"abstract":"<jats:p>Real-time systems must be properly validated and verified before their manufacturing and deployment in order to increase their reliability and reduce their maintenance cost. Models have been used for a long time to build complex systems, in virtually every engineering field. This is because they provide invaluable help in making important design decisions before the system is implemented. In this paper, the authors propose an approach based on model transformation to apply formal verification techniques to demonstrate the correctness of system designs. At the first step, they describe real-time systems by state chart (machine) diagrams, as source models to generate RT-Maude models (target models). The second step is to use the result models to verify the real-time systems against specified LTL properties using Maude LTL Model-Checker. This approach is illustrated through an example.<\/jats:p>","DOI":"10.4018\/ijitwe.2017100102","type":"journal-article","created":{"date-parts":[[2017,8,15]],"date-time":"2017-08-15T16:02:42Z","timestamp":1502812962000},"page":"22-41","source":"Crossref","is-referenced-by-count":0,"title":["A Model Transformation Approach for Specifying Real-Time Systems and Its Verification Using RT-Maude"],"prefix":"10.4018","volume":"12","author":[{"given":"Messaoud","family":"Bendiaf","sequence":"first","affiliation":[{"name":"Department of Computer Science University of Biskra, Biskra, Algeria"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Mustapha","family":"Bourahla","sequence":"additional","affiliation":[{"name":"Department of Computer Science University of M'sila, M'sila, Algeria"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Malika","family":"Boudia","sequence":"additional","affiliation":[{"name":"Department of Computer Science University of Biskra, Biskra, Algeria"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Seidali","family":"Rehab","sequence":"additional","affiliation":[{"name":"MISC Laboratory, University of Constantine 2 - Abdelhamid Mehri, Constantine, Algeria"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"2432","reference":[{"key":"IJITWE.2017100102-0","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-09156-3_38"},{"key":"IJITWE.2017100102-1","doi-asserted-by":"publisher","DOI":"10.1109\/ICSESS.2014.6933529"},{"key":"IJITWE.2017100102-2","doi-asserted-by":"crossref","unstructured":"Bezivin, J., Rumpe, B., Schurr, A., & Tratt, L. (2006). Model Transformations in Practice Workshop. In Bruel (Ed.), MoDELS 05 (Vol. 3844, pp. 120\u2013127). Springer.","DOI":"10.1007\/11663430_13"},{"key":"IJITWE.2017100102-3","doi-asserted-by":"crossref","unstructured":"Boucherit, A., Khebaba, A., & Belala, F. (2011, January). Rewriting Logic based Approach for the Formalization of Critical Systems based on Multi-Agent System. International Journal of Computer Applications, 13(2).","DOI":"10.5120\/1755-2392"},{"key":"IJITWE.2017100102-4","doi-asserted-by":"crossref","unstructured":"Bourahla, M. (2009, December). Modeling and Verification of Real-Time Embedded Systems. Proceedings of theThird International Symposium on Innovation in Information & Communication Technology, Philadelphia University, Amman, Jordan.","DOI":"10.14236\/ewic\/ISIICT2009.6"},{"key":"IJITWE.2017100102-5","doi-asserted-by":"crossref","unstructured":"Bouyer, P. (2009, March). Model-checking Timed Temporal Logics. Proceedings of the 5th Workshop on Methods for Modalities, ENTCS (Vol. 231, pp. 323-341).","DOI":"10.1016\/j.entcs.2009.02.044"},{"key":"IJITWE.2017100102-6","author":"G. C.Buttazzo","year":"2004","journal-title":"Hard Real-time Computing Systems: Predictable Scheduling Algorithms And Applications (Real-Time Systems Series)"},{"key":"IJITWE.2017100102-7","unstructured":"Charnecki, K., & Helsen, S. (2003, October). Classification of model transformation approaches. In OOPSLA 2003 Workshop on Generative Techniques in the Context of Model-Driven Architecture, Anaheim, CA, USA."},{"key":"IJITWE.2017100102-8","unstructured":"Clavel, M., Dur\u00e1n, F., Eker, S., Lincoln, P., Mart\u00ed-Oliet, N., Meseguer, J., & Talcott, C. (2007a, January). Maude Manual (Version 2.3), Retrieved September 20, 2016, from http:\/\/maude.cs.uiuc.edu"},{"key":"IJITWE.2017100102-9","author":"M.Clavel","year":"2007","journal-title":"All About Maude - A High-Performance Logical Framework, LNCS (Vol. 4350)"},{"key":"IJITWE.2017100102-10","unstructured":"Eclipse. (n. d.). Modeling M2T. Retrieved October 10, 2016, from https:\/\/eclipse.org\/modeling\/m2t\/"},{"key":"IJITWE.2017100102-11","unstructured":"Eker, S., Meseguer, J., & Sridharanarayanan, A. (2002). The Maude LTL model checker. In F. Gadducci and U. Montanari (Eds.), Proceedings of theFourth International Workshop on Rewriting Logic and its Applications, ENTCS (Vol. 71). Elsevier."},{"key":"IJITWE.2017100102-12","unstructured":"Erhan, L. (2014). A Comparison of Incremental Triple Graph Grammar Tools. Electronic Communications of the EASST, 67."},{"key":"IJITWE.2017100102-13","doi-asserted-by":"crossref","unstructured":"Friedenthal, S., & Wolfrom, J. (2010, July). Modeling with SysML. Proceedings of the Tutorial presented at INCOSE 2010 Symposium, Chicago, IL.","DOI":"10.1002\/j.2334-5837.2010.tb01160.x"},{"key":"IJITWE.2017100102-14","unstructured":"Hildebrandt, S., Lambers, L., Giese, H., Rieke, J., Greenyer, J., Sch\u00e4fer, W., . . . Sch\u00fcrr, A. (2013). A Survey of Triple Graph Grammar Tools. In Stevens and Terwilliger (Eds.), BX 13. ECEASST 57. EASST."},{"key":"IJITWE.2017100102-15","first-page":"1701","article-title":"Alvis models of safety critical systems state-base verification with nuXmv.","author":"B.Jerzy","year":"2016","journal-title":"Proceedings of the Federated Conference on Computer Science and Information Systems,"},{"key":"IJITWE.2017100102-16","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-10557-4_23"},{"key":"IJITWE.2017100102-17","doi-asserted-by":"publisher","DOI":"10.1016\/j.cosrev.2010.06.002"},{"key":"IJITWE.2017100102-18","doi-asserted-by":"crossref","unstructured":"Krzysztof, C., & Simon, H. (2006, July). Feature-based survey of model transformation approaches. IBM Systems Journal, 45(3), 621 \u2013 645.","DOI":"10.1147\/sj.453.0621"},{"key":"IJITWE.2017100102-19","doi-asserted-by":"crossref","unstructured":"Madari, I., Lengyel, L., & Mezei, G. (2008). Incremental model synchronization by Bi-directional model transformations. Proceedings of ICCC \u201808 - IEEE 6th International Conference on Computational Cybernetics, Stara Lesna, Slovakia (pp. 215-218).","DOI":"10.1109\/ICCCYB.2008.4721408"},{"key":"IJITWE.2017100102-20","doi-asserted-by":"crossref","unstructured":"Meseguer, J. (1998). Membership algebra as a logical framework for equational specification. In F. Parisi-Presicce (Ed.) Proc. of WADT\u201997, LNCS (Vol. 1376, pp. 18\u201361). Springer.","DOI":"10.1007\/3-540-64299-4_26"},{"key":"IJITWE.2017100102-21","unstructured":"Object Management Group OMG. (n. d.). Model Driven Architecture. Retrieved September 21, 2016, from http:\/\/www.omg.org\/mda\/"},{"key":"IJITWE.2017100102-22","doi-asserted-by":"publisher","DOI":"10.1007\/s10990-007-9001-5"},{"key":"IJITWE.2017100102-23","unstructured":"Peter, C. \u00d6. (2007, August). Real-Time Maude 2.3 Manual."},{"key":"IJITWE.2017100102-24","unstructured":"Rivera, J. E., Francisco, D., & Antonio, V. (2008). A Metamodel For Maude (tech. rep.). University of M\u00e1laga, Spain."},{"key":"IJITWE.2017100102-25","doi-asserted-by":"publisher","DOI":"10.1109\/ITSIM.2010.5561643"},{"key":"IJITWE.2017100102-26","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-59071-4_45"},{"key":"IJITWE.2017100102-27","unstructured":"OMG Systems Modeling Language. (n. d.). The Official OMG SysML site. Retrieved from http:\/\/www.omgsysml.org\/"},{"key":"IJITWE.2017100102-28","unstructured":"TGG Interpreter. (n. d.). home page. Retrieved from http:\/\/www-old.cs.uni-paderborn.de\/en\/research-group\/software-engineering\/research\/projects\/tgg-interpreter.html"},{"key":"IJITWE.2017100102-29","unstructured":"Xpand Documentation. Retrieved October 2, 2016, from http:\/\/ditec.um.es\/ssdd\/xpand_reference.pdf"}],"container-title":["International Journal of Information Technology and Web Engineering"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.igi-global.com\/viewtitle.aspx?TitleId=188380","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,5,6]],"date-time":"2022-05-06T09:56:41Z","timestamp":1651831001000},"score":1,"resource":{"primary":{"URL":"http:\/\/services.igi-global.com\/resolvedoi\/resolve.aspx?doi=10.4018\/IJITWE.2017100102"}},"subtitle":[""],"short-title":[],"issued":{"date-parts":[[2017,10]]},"references-count":30,"journal-issue":{"issue":"4"},"URL":"https:\/\/doi.org\/10.4018\/ijitwe.2017100102","relation":{},"ISSN":["1554-1045","1554-1053"],"issn-type":[{"value":"1554-1045","type":"print"},{"value":"1554-1053","type":"electronic"}],"subject":[],"published":{"date-parts":[[2017,10]]}}}