{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,12]],"date-time":"2025-11-12T14:06:56Z","timestamp":1762956416401},"reference-count":43,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2020,7,26]],"date-time":"2020-07-26T00:00:00Z","timestamp":1595721600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2020,7,26]],"date-time":"2020-07-26T00:00:00Z","timestamp":1595721600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["J Supercomput"],"published-print":{"date-parts":[[2021,3]]},"DOI":"10.1007\/s11227-020-03386-9","type":"journal-article","created":{"date-parts":[[2020,7,26]],"date-time":"2020-07-26T19:02:22Z","timestamp":1595790142000},"page":"3110-3143","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":6,"title":["An event-based approach for formally verifying runtime adaptive real-time systems"],"prefix":"10.1007","volume":"77","author":[{"given":"Nissaf","family":"Fredj","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Yessine","family":"Hadj Kacem","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Mohamed","family":"Abid","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2020,7,26]]},"reference":[{"issue":"10","key":"3386_CR1","doi-asserted-by":"publisher","first-page":"32","DOI":"10.1109\/MC.2007.364","volume":"40","author":"TA Henzinger","year":"2007","unstructured":"Henzinger TA, Sifakis J (2007) The discipline of embedded systems design. IEEE Soc Comput 40(10):32\u201340","journal-title":"IEEE Soc Comput"},{"key":"#cr-split#-3386_CR2.1","doi-asserted-by":"crossref","unstructured":"Magdich A, Kacem YH, Mahfoudhi A, Kerboeuf Ml (2014) A uml\/marte-based design pattern for semi-partitioned scheduling analysis. In: Sumitra R","DOI":"10.1109\/WETICE.2014.9"},{"key":"#cr-split#-3386_CR2.2","unstructured":"(ed) 2014 IEEE 23rd international WETICE conference (WETICE 2014), Parma, Italy, 23-25 June, 2014. IEEE Computer Society, pp 300-305"},{"key":"3386_CR3","doi-asserted-by":"crossref","unstructured":"Devaraj R (2020) A solution to drawbacks in capturing execution requirements on heterogeneous platforms. J Supercomput 76(4)","DOI":"10.1007\/s11227-020-03145-w"},{"issue":"2","key":"3386_CR4","doi-asserted-by":"publisher","first-page":"25","DOI":"10.1109\/MC.2006.58","volume":"39","author":"DC Schmidt","year":"2006","unstructured":"Schmidt DC (2006) Model-driven engineering. IEEE Computer 39(2):25","journal-title":"IEEE Computer"},{"issue":"4","key":"3386_CR5","first-page":"8012","volume":"76","author":"A Bernal","year":"2020","unstructured":"Bernal A, Emilia CM, Nunez A, Canizares PC, Valero V (2020) Improving cloud architectures using UML profiles and M2T transformation techniques. J Supercomput 76(4):8012\u20138058","journal-title":"J Supercomput"},{"issue":"3","key":"3386_CR6","doi-asserted-by":"publisher","first-page":"1478","DOI":"10.1007\/s11227-011-0557-9","volume":"59","author":"A Mahfoudhi","year":"2012","unstructured":"Mahfoudhi A, Kacem YH, Karamti W, Abid M (2012) Compositional specification of real time embedded systems by priority time petri nets. J Supercomput 59(3):1478\u20131503","journal-title":"J Supercomput"},{"issue":"4","key":"3386_CR7","first-page":"6194","volume":"28","author":"A Amr","year":"2020","unstructured":"Amr A, Enrique A, Gabriel L (2020) A component-based study of energy consumption for sequential and parallel genetic algorithms. J Supercomput 28(4):6194\u20136219","journal-title":"J Supercomput"},{"issue":"6","key":"3386_CR8","first-page":"1","volume":"76","author":"A Ghavidel","year":"2019","unstructured":"Ghavidel A, Sedaghat Y, Naghibzadeh M (2019) Hybrid scheduling to enhance reliability of real-time tasks running on reconfigurable devices. J Supercomput 76(6):1","journal-title":"J Supercomput"},{"key":"3386_CR9","doi-asserted-by":"crossref","unstructured":"Duhil C, Babau J-P, Lepicier E, Voirin J-L, Navas J (2020) Chaining model transformations for system model verification: application to verify capella model with simulink. In: International conference on model-driven engineering and software development (MODELSWARD 2020)","DOI":"10.5220\/0008902302790286"},{"key":"3386_CR10","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/s10586-018-02903-z","volume":"23","author":"MB Said","year":"2020","unstructured":"Said MB, Kacem YH, Kerboeuf M, Abid M (2020) An MDE-based approach for self-adaptive RTES model generation. Cluster Comput 23:1\u201327","journal-title":"Cluster Comput"},{"issue":"1","key":"3386_CR11","doi-asserted-by":"publisher","first-page":"28","DOI":"10.1504\/IJCAT.2018.090029","volume":"57","author":"M Hachicha","year":"2018","unstructured":"Hachicha M, Halima RB, Kacem AH (2018) Modelling, specifying and verifying selfadaptive systems instantiating mape patterns. Int J Comput Appl Technol 57(1):28\u201344","journal-title":"Int J Comput Appl Technol"},{"issue":"3","key":"3386_CR12","first-page":"117","volume":"10","author":"A Masrur","year":"2017","unstructured":"Masrur A, Kit M, Matena V, Buresb T, Hardt W (2017) Component-based design of cyber-physical applications with safety-critical requirements. J Microprocess Microsyst 10(3):117","journal-title":"J Microprocess Microsyst"},{"key":"3386_CR13","unstructured":"OMG Object\u00a0Management Group (2011) A UML profile for MARTE: modeling and analysis of real-time embedded systems, ptc\/2011-06-02. Object Management Group"},{"key":"#cr-split#-3386_CR14.1","doi-asserted-by":"crossref","unstructured":"Magdich A, Kacem YH, Mahfoudhi A, Kerboeuf M (2014) A UML\/MARTE-based design pattern for semi-partitioned scheduling analysis. In: Sumitra R","DOI":"10.1109\/WETICE.2014.9"},{"key":"#cr-split#-3386_CR14.2","unstructured":"(ed) IEEE 23rd international WETICE conference (WETICE 2014), Parma, Italy, 23-25 June, 2014. IEEE Computer Society, pp 300-305"},{"key":"3386_CR15","doi-asserted-by":"publisher","first-page":"3637","DOI":"10.1007\/s11227-015-1455-3","volume":"71","author":"A Mahfoudhi","year":"2015","unstructured":"Mahfoudhi A, Karamti W (2015) Transformation process of rts scheduling analysis requirements from UML\/MARTE to dynamic priority time petri nets. J Supercomput 71:3637\u20133667","journal-title":"J Supercomput"},{"issue":"6","key":"3386_CR16","first-page":"365","volume":"68","author":"S Loukil","year":"2016","unstructured":"Loukil S, Kallel S, Jmaiel M (2016) An approach based on runtime models for developing dynamically adaptive systems. J Future Gener Comput Syst 68(6):365\u2013375","journal-title":"J Future Gener Comput Syst"},{"issue":"10","key":"3386_CR17","doi-asserted-by":"publisher","first-page":"44","DOI":"10.1109\/MC.2009.327","volume":"42","author":"B Morin","year":"2009","unstructured":"Morin B, Barais O, Jezequel J-M, Fleurey F, Solberg A (2009) A models at run.time to support dynamic adaptation. Computer 42(10):44\u201351","journal-title":"Computer"},{"key":"3386_CR18","doi-asserted-by":"crossref","unstructured":"Vardhan V, Sachs DG, Yuan W, Harris AF, Adve SV, Jones DL, Kravets RH, Nahrstedt KM (2009) Integrating fine-grained application adaptation with global adaptation for saving energy. University of Illinois at UrbanaChampaign","DOI":"10.1504\/IJES.2009.027939"},{"key":"3386_CR19","doi-asserted-by":"crossref","unstructured":"Fredj N, Kacem YHADJ, Abid M (2018) Runtime uml marte extensions for the design of adaptive rte systems. In: 18th International conference on intelligent systems design and applications (ISDA), 2018, Vellore, India","DOI":"10.1007\/978-3-030-16660-1_8"},{"key":"3386_CR20","unstructured":"Abrial J-R (2010) Modeling in event-b: system and software engineering. Cambridge University Press, New York, NY, USA. ISBN: 0521895561 9780521895569"},{"key":"3386_CR21","doi-asserted-by":"publisher","first-page":"447","DOI":"10.1007\/s10009-010-0145-y","volume":"12","author":"JR Abrial","year":"2010","unstructured":"Abrial JR, Butler M, Hallerstede S, Hoang TS, Mehta F, Voisin L (2010) Rodin: an open toolset for modelling and reasoning in eventb. Int J Softw Tools Technol Transf 12:447\u2013466","journal-title":"Int J Softw Tools Technol Transf"},{"key":"3386_CR22","doi-asserted-by":"crossref","unstructured":"Al\u00a0Assadi WK, Gandla S, Sahra SS, Dugganapally IP (2009) Design and FPGA prototyping of a flood prediction system. In: 12th international IEEE conference on intelligent transportation systems, pp 1\u20136","DOI":"10.1109\/ITSC.2009.5309516"},{"key":"3386_CR23","unstructured":"Said MB, Kacem YH, Amor NB, Abid M (2013) High level design of adaptive real-time embedded systems a survey. In: MODELSWARD: international conference on model-driven engineering and software development, pp 341\u2013350"},{"key":"3386_CR24","first-page":"97","volume":"2008","author":"F Fleurey","year":"2008","unstructured":"Fleurey F, Dehlen V, Bencomo N, Morin B, Jezequel JM (2008) Modeling and validating dynamic adaptation. Int Conf Model Driven Eng Lang Syst MODELS 2008:97\u2013108","journal-title":"Int Conf Model Driven Eng Lang Syst MODELS"},{"key":"3386_CR25","unstructured":"Morin B (2010) Leveraging models from design time to runtime to support dynamic variability. University of Rennes, Ph.D. thesis"},{"key":"3386_CR26","doi-asserted-by":"publisher","first-page":"149","DOI":"10.1016\/j.scico.2017.09.006","volume":"161","author":"S Costiou","year":"2018","unstructured":"Costiou S, Kerboeuf M, Cavarle G, Plantec A (2018) Lub: A pattern for fine grained behavior adaptation at runtime. Sci. Comput. Program. 161:149\u2013171","journal-title":"Sci. Comput. Program."},{"key":"3386_CR27","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1007\/s10703-019-00337-w","volume":"54","author":"C Sanchez","year":"2019","unstructured":"Sanchez C, Schneider G, Ahrendt W, Bartocci E, Bianculli D, Colombo C, Falcone Y, Francalanza A, Krstic S, Loureno JM, Nickovic D, Pace GJ, Rufino J, Signoles J, Traytel D, Weiss A (2019) A survey of challenges for runtime verification from advanced application domains (beyond software). Int J Form Methods Syst Des 54:279\u2013335","journal-title":"Int J Form Methods Syst Des"},{"issue":"6","key":"3386_CR28","doi-asserted-by":"publisher","first-page":"738","DOI":"10.1504\/IJES.2019.103991","volume":"11","author":"R Mzid","year":"2019","unstructured":"Mzid R, Mraidha C, Babau J-P, Abid M (2019) From real-time design model to RTOS-specific models: a model-driven methodology. Int J Embed Syst 11(6):738\u2013754","journal-title":"Int J Embed Syst"},{"key":"3386_CR29","doi-asserted-by":"crossref","unstructured":"Weyns D, Malek S, Andersson J (2010) Forms: a formal reference model for self-adaptation. In: Proceedings of the 7th international conference on autonomic computing (ICAC10), New York, p 205214","DOI":"10.1145\/1809049.1809078"},{"issue":"4","key":"3386_CR30","first-page":"626643","volume":"28","author":"PA Jeannette","year":"1996","unstructured":"Jeannette PA, Wing Edmund M, Clarke M (1996) Formal methods: state of the art and future directions. ACM Comput Surv (CSUR) 28(4):626643","journal-title":"ACM Comput Surv (CSUR)"},{"key":"3386_CR31","doi-asserted-by":"crossref","unstructured":"Bowen J, Stavridou V (1993) Formal methods in safety-critical standards. Softw Eng J, 168177","DOI":"10.1109\/SESS.1993.263953"},{"issue":"1","key":"3386_CR32","doi-asserted-by":"publisher","first-page":"33","DOI":"10.1016\/0164-1212(92)90045-L","volume":"18","author":"S Ostroff Jonathan","year":"1992","unstructured":"Ostroff Jonathan S (1992) Formal methods for the specification and design of real-time safety critical systems. J Syst Softw 18(1):33\u201360","journal-title":"J Syst Softw"},{"issue":"3","key":"3386_CR33","doi-asserted-by":"publisher","first-page":"115","DOI":"10.1145\/2724719","volume":"10","author":"DIDACGILDELA IGLESIA","year":"2015","unstructured":"IGLESIA DIDACGILDELA, WEYNS DANNY (2015) Mape-k formal templates to rigorously design behaviors for self-adaptive systems. ACM Trans Auton Adapt Syst 10(3):115","journal-title":"ACM Trans Auton Adapt Syst"},{"key":"3386_CR34","doi-asserted-by":"crossref","unstructured":"Arcaini P, Riccobene E, Scandurra P (2015) Modeling and analyzing mape-k feedback loops for self-adaptation. In: International symposium on software engineering for adaptive and self-managing systems (SEAMS15). IEEE, Piscataway, NJ, USA, p 1323","DOI":"10.1109\/SEAMS.2015.10"},{"key":"3386_CR35","doi-asserted-by":"crossref","unstructured":"Younes AB, Ayed Leila JB (2007) Using uml activity diagrams and event b for distributed and parallel applications. In: International computer software and applications conference(COMPSAC)","DOI":"10.1109\/COMPSAC.2007.233"},{"key":"3386_CR36","doi-asserted-by":"crossref","unstructured":"Tarasyuk A, Pereverzeva I, Troubitsyna E, Latvala T, Nummila L (2012) Formal development and assessment of a reconfigurable on board satellite system. In: International conference on computer safety, reliability, and security, pp 210\u2013222","DOI":"10.1007\/978-3-642-33678-2_18"},{"key":"3386_CR37","doi-asserted-by":"crossref","unstructured":"Babin G, Ameur Yamine AIT, Pantel M (2016) Correct instantiation of a system reconfiguration pattern: a proof and refinement based approach. In: International symposium on high assurance systems engineering","DOI":"10.1109\/HASE.2016.47"},{"issue":"1","key":"3386_CR38","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1007\/978-3-031-02549-5","volume":"3","author":"M Brambilla","year":"2012","unstructured":"Brambilla M, Cabot J, Wimmer M (2012) Model driven software engineering in practice. Synth Lect Softw Eng 3(1):1\u2013207","journal-title":"Synth Lect Softw Eng"},{"key":"3386_CR39","doi-asserted-by":"publisher","first-page":"83","DOI":"10.1016\/j.infsof.2018.01.002","volume":"997","author":"A Magdich","year":"2018","unstructured":"Magdich A, Kacem YH, Kerboeuf M, Mahfoudhi A, Abid M (2018) A design pattern-based approach for automatic choice of semi-partitioned and global scheduling algorithms. Inf Softw Technol 997:83\u201398","journal-title":"Inf Softw Technol"},{"key":"3386_CR40","doi-asserted-by":"crossref","unstructured":"Merz S (2000) Model checking: a tutorial overview. In: 4th summer school on modeling and verification of parallel processes. MOVEP, Nantes, France, pp 3\u201338","DOI":"10.1007\/3-540-45510-8_1"},{"issue":"2","key":"3386_CR41","doi-asserted-by":"publisher","first-page":"01","DOI":"10.1145\/1516533.1516538","volume":"4","author":"M Salehie","year":"2009","unstructured":"Salehie M, Tahvildari L (2009) Self adaptive software: landscape and research challenges. ACM Trans Auton Adapt Syst 4(2):01\u201342","journal-title":"ACM Trans Auton Adapt Syst"}],"container-title":["The Journal of Supercomputing"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s11227-020-03386-9.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s11227-020-03386-9\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s11227-020-03386-9.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,11,4]],"date-time":"2022-11-04T14:56:15Z","timestamp":1667573775000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s11227-020-03386-9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,7,26]]},"references-count":43,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2021,3]]}},"alternative-id":["3386"],"URL":"https:\/\/doi.org\/10.1007\/s11227-020-03386-9","relation":{},"ISSN":["0920-8542","1573-0484"],"issn-type":[{"value":"0920-8542","type":"print"},{"value":"1573-0484","type":"electronic"}],"subject":[],"published":{"date-parts":[[2020,7,26]]},"assertion":[{"value":"26 July 2020","order":1,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}