{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,10]],"date-time":"2025-10-10T07:15:14Z","timestamp":1760080514034,"version":"3.37.3"},"reference-count":61,"publisher":"Sociedade Brasileira de Computacao - SB","issue":"1","license":[{"start":{"date-parts":[[2021,5,24]],"date-time":"2021-05-24T00:00:00Z","timestamp":1621814400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2021,5,24]],"date-time":"2021-05-24T00:00:00Z","timestamp":1621814400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"DOI":"10.13039\/501100011914","name":"M?lardalens h?gskola","doi-asserted-by":"publisher","award":["111"],"award-info":[{"award-number":["111"]}],"id":[{"id":"10.13039\/501100011914","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["J Internet Serv Appl"],"published-print":{"date-parts":[[2021,12]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Software systems are complicated, and the scientific and engineering methodologies for software development are relatively young. Cyber-physical systems are now in every corner of our lives, and we need robust methods for handling the ever-increasing complexity of their software systems. Model-Driven Development is a promising approach to tackle the complexity of systems through the concept of abstraction, enabling analysis at earlier phases of development. In this paper, we propose a model-driven approach with a focus on guaranteeing safety using formal verification. Cyber-physical systems are distributed, concurrent, asynchronous and event-based reactive systems with timing constraints. The actor-based textual modeling language, Rebeca, with model checking support is used for formal verification. Starting from structured requirements and system architecture design the behavioral models, including Rebeca models, are built. Properties of interest are also derived from the structured requirements, and then model checking is used to formally verify the properties. This process can be performed in iterations until satisfaction of desired properties are ensured, and possible ambiguities and inconsistencies in requirements are resolved. The formally verified models can then be used to develop the executable code. The Rebeca models include the details of the signals and messages that are passed at the network level including the timing, and this facilitates the generation of executable code. The natural mappings among the models for requirements, the formal models, and the executable code improve the effectiveness and efficiency of the approach.<\/jats:p>","DOI":"10.1186\/s13174-021-00132-z","type":"journal-article","created":{"date-parts":[[2021,5,24]],"date-time":"2021-05-24T05:02:39Z","timestamp":1621832559000},"update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":6,"title":["Towards a Verification-Driven Iterative Development of Software for Safety-Critical Cyber-Physical Systems"],"prefix":"10.5753","volume":"12","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-5478-0987","authenticated-orcid":false,"given":"Marjan","family":"Sirjani","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Luciana","family":"Provenzano","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Sara Abbaspour","family":"Asadollah","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Mahshid Helali","family":"Moghadam","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Mehrdad","family":"Saadatmand","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"3742","published-online":{"date-parts":[[2021,5,24]]},"reference":[{"key":"132_CR1","doi-asserted-by":"crossref","unstructured":"Lee EA. Cyber physical systems: Design challenges. In: 2008 11th IEEE International Symposium on Object and Component-oriented Real-time Distributed Computing (ISORC). IEEE: 2008. p. 363\u20139.","DOI":"10.1109\/ISORC.2008.25"},{"issue":"5","key":"132_CR2","doi-asserted-by":"publisher","first-page":"33","DOI":"10.1109\/MC.2006.180","volume":"39","author":"EA Lee","year":"2006","unstructured":"Lee EA. The problem with threads. Computer. 2006; 39(5):33\u201342.","journal-title":"Computer"},{"key":"132_CR3","volume-title":"System Design, Modeling, and Simulation Using Ptolemy II, vol. 1","author":"C Ptolemaeus","year":"2014","unstructured":"Ptolemaeus C. System Design, Modeling, and Simulation Using Ptolemy II, vol. 1. Berkeley: Ptolemy.org; 2014."},{"key":"132_CR4","doi-asserted-by":"crossref","unstructured":"Lee EA, Sirjani M. What good are models? In: Formal Aspects of Component Software - 15th International Conference, FACS 2018, Pohang, South Korea, October 10-12, 2018, Proceedings. Lecture Notes in Computer Science, vol. 11222. Springer: 2018. p. 3\u201331.","DOI":"10.1007\/978-3-030-02146-7_1"},{"key":"132_CR5","volume-title":"Principles of Modeling","author":"M Sirjani","year":"2018","unstructured":"Sirjani M. Power is overrated, go for friendliness! expressiveness, faithfulness, and usability in modeling: the actor experience. In: Principles of Modeling. Cham: Springer: 2018. p. 423\u201348."},{"key":"132_CR6","unstructured":"Holzmann G. Spin Model Checker, the: Primer and Reference Manual. 2003."},{"issue":"4","key":"132_CR7","doi-asserted-by":"publisher","first-page":"410","DOI":"10.1007\/s100090050046","volume":"2","author":"A Cimatti","year":"2000","unstructured":"Cimatti A, Clarke E, Giunchiglia F, Roveri M. Nusmv: a new symbolic model checker. International Journal on Software Tools for Technology Transfer. 2000; 2(4):410\u201325.","journal-title":"International Journal on Software Tools for Technology Transfer"},{"issue":"1","key":"132_CR8","doi-asserted-by":"publisher","first-page":"134","DOI":"10.1007\/s100090050010","volume":"1","author":"KG Larsen","year":"1997","unstructured":"Larsen KG, Pettersson P, Yi W. Uppaal in a nutshell. Int J Softw Tools Technol Tran (STTT). 1997; 1(1):134\u201352.","journal-title":"Int J Softw Tools Technol Tran (STTT)"},{"key":"132_CR9","doi-asserted-by":"publisher","first-page":"41","DOI":"10.1016\/j.scico.2014.01.008","volume":"89","author":"AH Reynisson","year":"2014","unstructured":"Reynisson AH, Sirjani M, Aceto L, Cimini M, Jafari A, Ing\u00f3lfsd\u00f3ttir A, Sigurdarson SH. Modelling and simulation of asynchronous real-time systems using timed Rebeca. Sci Comput Program. 2014; 89:41\u201368.","journal-title":"Sci Comput Program"},{"key":"132_CR10","volume-title":"Theory and Practice of Formal Methods","author":"M Sirjani","year":"2016","unstructured":"Sirjani M, Khamespanah E. On time actors. In: Theory and Practice of Formal Methods. Cham: Springer: 2016. p. 373\u2013392."},{"key":"132_CR11","doi-asserted-by":"publisher","first-page":"184","DOI":"10.1016\/j.scico.2014.07.005","volume":"98","author":"E Khamespanah","year":"2015","unstructured":"Khamespanah E, Sirjani M, Sabahi-Kaviani Z, Khosravi R, Izadi M. Timed Rebeca schedulability and deadlock freedom analysis using bounded floating time transition system. Sci Comput Program. 2015; 98:184\u2013204.","journal-title":"Sci Comput Program"},{"issue":"7","key":"132_CR12","doi-asserted-by":"publisher","first-page":"1068","DOI":"10.3390\/math8071068","volume":"8","author":"M Sirjani","year":"2020","unstructured":"Sirjani M, Lee EA, Khamespanah E. Verification of cyberphysical systems. Mathematics. 2020; 8(7):1068.","journal-title":"Mathematics"},{"key":"132_CR13","volume-title":"International Conference on Coordination Languages and Models","author":"M Zarneshan","year":"2020","unstructured":"Zarneshan M, Ghassemi F, Sirjani M. Formal modeling and analysis of medical systems. In: International Conference on Coordination Languages and Models. Cham: Springer: 2020. p. 386\u2013402."},{"key":"132_CR14","volume-title":"International Conference on Formal Methods for Industrial Critical Systems","author":"F Moradi","year":"2020","unstructured":"Moradi F, Asadollah SA, Sedaghatbaf A, \u010cau\u0161evi\u0107 A, Sirjani M, Talcott C. An actor-based approach for security analysis of cyber-physical systems. In: International Conference on Formal Methods for Industrial Critical Systems. Cham: Springer: 2020. p. 130\u201347."},{"key":"132_CR15","unstructured":"Rebeca. Rebeca Homepage. http:\/\/www.rebeca-lang.org\/. Retrieved July 2019."},{"issue":"4","key":"132_CR16","first-page":"385","volume":"63","author":"M Sirjani","year":"2004","unstructured":"Sirjani M, Movaghar A, Shali A, De Boer FS. Modeling and verification of reactive systems using Rebeca. Fundam Informaticae. 2004; 63(4):385\u2013410.","journal-title":"Fundam Informaticae"},{"key":"132_CR17","volume-title":"International Symposium on Formal Methods for Components and Objects","author":"M Sirjani","year":"2006","unstructured":"Sirjani M. Rebeca: Theory, applications, and tools. In: International Symposium on Formal Methods for Components and Objects. Berlin: Springer: 2006. p. 102\u201326."},{"issue":"5","key":"132_CR18","first-page":"76","volume":"50","author":"FS de Boer","year":"2017","unstructured":"de Boer FS, Serbanescu V, H\u00e4hnle R, Henrio L, Rochas J, Din CC, Johnsen EB, Sirjani M, Khamespanah E, Fernandez-Reyes K, Yang AM. A survey of active object languages. ACM Comput Surv. 2017; 50(5):76\u201317639.","journal-title":"ACM Comput Surv"},{"key":"132_CR19","unstructured":"Sirjani M, Provenzano L, Asadollah SA, Moghadam MH. From requirements to verifiable executable models using Rebeca. In: International Workshop on Automated and Verifiable Software sYstem DEvelopment: 2019. http:\/\/www.es.mdh.se\/publications\/5645-."},{"key":"132_CR20","doi-asserted-by":"crossref","unstructured":"Provenzano L, H\u00e4nninen K, Zhou J, Lundqvist K. An ontological approach to elicit safety requirements. In: 2017 24th Asia-Pacific Software Engineering Conference (APSEC). IEEE: 2017. p. 713\u20138.","DOI":"10.1109\/APSEC.2017.91"},{"key":"132_CR21","unstructured":"Firesmith DG. A taxonomy of safety-related requirements. Requir Eng. 2004. White paper - Carnegie Mellon University."},{"key":"132_CR22","doi-asserted-by":"crossref","unstructured":"Zhou J, H\u00e4nninen K, Lundqvist K, Provenzano L. An ontological approach to hazard identification for safety-critical systems. In: 2017 Second International Conference on Reliability Systems Engineering (ICRSE). IEEE: 2017. p. 1\u20137.","DOI":"10.1109\/ICRSE.2017.8030746"},{"key":"132_CR23","doi-asserted-by":"crossref","unstructured":"Zhou J, H\u00e4nninen K, Lundqvist K, Provenzano L. An ontological approach to identify the causes of hazards for safety-critical systems. In: 2017 2nd International Conference on System Reliability and Safety (ICSRS). IEEE: 2017. p. 405\u201313.","DOI":"10.1109\/ICSRS.2017.8272856"},{"key":"132_CR24","unstructured":"Fowler M. ThoughtWorks: GivenWhenThen. 2013. https:\/\/martinfowler.com\/bliki\/GivenWhenThen.html. Retrieved July 2019."},{"key":"132_CR25","unstructured":"North D. Introducing BDD. Better Softw Mag. 2006. https:\/\/dannorth.net\/introducing-bdd\/. Retrieved July 2019."},{"key":"132_CR26","volume-title":"ACTORS - a Model of Concurrent Computation in Distributed Systems. MIT Press series in artificial intelligence","author":"GA Agha","year":"1990","unstructured":"Agha GA. ACTORS - a Model of Concurrent Computation in Distributed Systems. MIT Press series in artificial intelligence. Cambridge: MIT Press; 1990."},{"key":"132_CR27","unstructured":"Hewitt C. Description and theoretical analysis (using schemata) of PLANNER: A language for proving theorems and manipulating models in a robot. Technical report, MIT Artificial Intelligence Technical Report. 1972."},{"issue":"5","key":"132_CR28","doi-asserted-by":"publisher","first-page":"547","DOI":"10.1007\/s10009-017-0480-3","volume":"20","author":"E Khamespanah","year":"2018","unstructured":"Khamespanah E, Sirjani M, Mechitov K, Agha G. Modeling and analyzing real-time wireless sensor and actuator networks using actors and model checking. STTT. 2018; 20(5):547\u201361.","journal-title":"STTT"},{"issue":"6","key":"132_CR29","doi-asserted-by":"publisher","first-page":"1051","DOI":"10.1007\/s00165-017-0429-z","volume":"29","author":"B Yousefi","year":"2017","unstructured":"Yousefi B, Ghassemi F, Khosravi R. Modeling and efficient verification of wireless ad hoc networks. Form Asp Comput. 2017; 29(6):1051\u201386.","journal-title":"Form Asp Comput"},{"key":"132_CR30","first-page":"1","volume":"66","author":"Z Sharifi","year":"2013","unstructured":"Sharifi Z, Mosaffa M, Mohammadi S, Sirjani M. Functional and performance analysis of network-on-chips using actor-based modeling and formal verification. ECEASST. 2013; 66:1\u201316.","journal-title":"ECEASST"},{"key":"132_CR31","doi-asserted-by":"crossref","unstructured":"Nigro L, Sciammarella PF. Time synchronization in wireless sensor networks: A modeling and analysis experience using theatre. In: 2018 IEEE\/ACM 22nd International Symposium on Distributed Simulation and Real Time Applications (DS-RT). IEEE: 2018. p. 1\u20138.","DOI":"10.1109\/DISTRA.2018.8600934"},{"key":"132_CR32","volume-title":"2019 Forum for Specification and Design Languages (FDL)","author":"M Lohstroh","year":"2019","unstructured":"Lohstroh M, Lee EA. Deterministic actors. In: 2019 Forum for Specification and Design Languages (FDL). Southampton: IEEE: 2019. p. 1\u20138."},{"key":"132_CR33","volume-title":"Proceedings of the 56th Annual Design Automation Conference 2019, DAC 2019","author":"M Lohstroh","year":"2019","unstructured":"Lohstroh M, Schoeberl M, Goens A, Wasicek A, Gill C, Sirjani M, Lee EA. Actors revisited for time-critical systems. In: Proceedings of the 56th Annual Design Automation Conference 2019, DAC 2019. Las Vegas: IEEE: 2019. p. 1\u20134."},{"key":"132_CR34","unstructured":"Rebeca. Afra Tool. 2019. http:\/\/rebeca-lang.org\/alltools\/Afra. Retrieved July 2019."},{"key":"132_CR35","unstructured":"Rebeca. RMC Tool. 2016. http:\/\/rebeca-lang.org\/alltools\/RMC. Retrieved July 2019."},{"key":"132_CR36","unstructured":"Wikipedia. RailwayPlatform. 2019. https:\/\/en.wikipedia.org\/wiki\/Railway_platform. Retrieved July 2019."},{"key":"132_CR37","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-28554-7","volume-title":"Model-driven Software Development","author":"S Beydeda","year":"2005","unstructured":"Beydeda S, Book M, Gruhn V, et al.Model-driven Software Development. Heidelberg: Springer; 2005."},{"issue":"1","key":"132_CR38","doi-asserted-by":"publisher","first-page":"91","DOI":"10.1007\/s10270-016-0523-3","volume":"17","author":"G Liebel","year":"2018","unstructured":"Liebel G, Marko N, Tichy M, Leitner A, Hansson J. Model-based engineering in the embedded systems domain: an industrial survey on the state-of-practice. Softw Syst Model. 2018; 17(1):91\u2013113.","journal-title":"Softw Syst Model"},{"key":"132_CR39","volume-title":"Proceedings of the 47th Design Automation Conference (DAC \u201910)","author":"EA Lee","year":"2010","unstructured":"Lee EA. CPS Foundations. In: Proceedings of the 47th Design Automation Conference (DAC \u201910). New York: Association for Computing Machinery: 2010. p. 737\u201342."},{"key":"132_CR40","doi-asserted-by":"crossref","unstructured":"Object Management Group. OMG Systems Modeling Language v1.5. 2017. https:\/\/sysmlforum.com\/sysml-specs\/. Retrieved July 2019.","DOI":"10.1016\/B978-1-78548-171-0.50001-3"},{"key":"132_CR41","unstructured":"Object Management Group. UML profile for MARTE, beta 2. 2008. https:\/\/www.omg.org\/omgmarte\/Specification.htm. Retrieved July 2019."},{"issue":"1","key":"132_CR42","first-page":"161","volume":"12","author":"R Baheti","year":"2011","unstructured":"Baheti R, Gill H. Cyber-physical systems. Impact Control Technol. 2011; 12(1):161\u20136.","journal-title":"Impact Control Technol"},{"key":"132_CR43","doi-asserted-by":"publisher","DOI":"10.1201\/9781315218335","volume-title":"Modeling and Simulation of Systems Using MATLAB and Simulink","author":"DK Chaturvedi","year":"2017","unstructured":"Chaturvedi DK. Modeling and Simulation of Systems Using MATLAB and Simulink. Boca Raton: CRC press; 2017."},{"key":"132_CR44","volume-title":"Proceedings of the 12th International Workshop on Search-Based Software Testing (SBST \u201919)","author":"S Nejati","year":"2019","unstructured":"Nejati S. Testing cyber-physical systems via evolutionary algorithms and machine learning. In: Proceedings of the 12th International Workshop on Search-Based Software Testing (SBST \u201919). Montreal: IEEE Press: 2019. p. 1."},{"key":"132_CR45","volume-title":"Search Based Software Engineering","author":"R Matinnejad","year":"2013","unstructured":"Matinnejad R, Nejati S, Briand L, Bruckmann T, Poull C. Automated model-in-the-loop testing of continuous controllers using search In: Ruhe G, Zhang Y, editors. Search Based Software Engineering. Berlin, Heidelberg: Springer: 2013. p. 141\u201357."},{"key":"132_CR46","doi-asserted-by":"crossref","unstructured":"Marinescu R, Saadatmand M, Bucaioni A, Seceleanu C, Pettersson P. A model-based testing framework for automotive embedded systems. In: 2014 40th EUROMICRO Conference on Software Engineering and Advanced Applications. IEEE: 2014. p. 38\u201347.","DOI":"10.1109\/SEAA.2014.70"},{"key":"132_CR47","volume-title":"International Conference on TOOLS and Algorithms for the Construction and Analysis of Systems","author":"S Kong","year":"2015","unstructured":"Kong S, Gao S, Chen W, Clarke E. dreach: \u03b4-reachability analysis for hybrid systems. In: International Conference on TOOLS and Algorithms for the Construction and Analysis of Systems. Berlin: Springer: 2015. p. 200\u20135."},{"key":"132_CR48","volume-title":"Proceedings of the 40th International Conference on Software Engineering (ICSE \u201918)","author":"SA Chowdhury","year":"2018","unstructured":"Chowdhury SA, Mohian S, Mehra S, Gawsane S, Johnson TT, Csallner C. Automatically finding bugs in a commercial cyber-physical system development tool chain with slforge. In: Proceedings of the 40th International Conference on Software Engineering (ICSE \u201918). New York: Association for Computing Machinery: 2018. p. 981\u201392."},{"key":"132_CR49","unstructured":"MathWorks. Stateflow: Model and simulate decision logic using state machines and flow charts. 2018. https:\/\/www.mathworks.com\/products\/stateflow.html. Retrieved July 2019."},{"key":"132_CR50","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/j.scico.2017.11.004","volume":"153","author":"E Khamespanah","year":"2018","unstructured":"Khamespanah E, Khosravi R, Sirjani M. An efficient TCTL model checking algorithm and a reduction technique for verification of timed actor models. Sci Comput Program. 2018; 153:1\u201329.","journal-title":"Sci Comput Program"},{"key":"132_CR51","volume-title":"International Conference on Modelling Techniques and Tools for Computer Performance Evaluation","author":"M Kwiatkowska","year":"2002","unstructured":"Kwiatkowska M, Norman G, Parker D. PRISM: Probabilistic symbolic model checker. In: International Conference on Modelling Techniques and Tools for Computer Performance Evaluation. Berlin: Springer: 2002. p. 200\u20134."},{"issue":"2","key":"132_CR52","doi-asserted-by":"publisher","first-page":"151","DOI":"10.1108\/IJWIS-02-2014-0004","volume":"10","author":"T Ando","year":"2014","unstructured":"Ando T, Yatsu H, Kong W, Hisazumi K, Fukuda A. Translation rules of SysML state machine diagrams into CSP# toward formal model checking. Int J Web Inf Syst. 2014; 10(2):151\u201369.","journal-title":"Int J Web Inf Syst"},{"issue":"1-2","key":"132_CR53","doi-asserted-by":"publisher","first-page":"83","DOI":"10.1007\/s11334-009-0116-1","volume":"6","author":"HH Hansen","year":"2010","unstructured":"Hansen HH, Ketema J, Luttik B, Mousavi MR, Van De Pol J. Towards model checking executable UML specifications in mCRL2. Innov Syst Softw Eng. 2010; 6(1-2):83\u201390.","journal-title":"Innov Syst Softw Eng"},{"key":"132_CR54","volume-title":"2009 Third International Conference on Digital Society","author":"E Andrade","year":"2009","unstructured":"Andrade E, Maciel P, Callou G, Nogueira B. A methodology for mapping SysML activity diagram to time petri net for requirement validation of embedded real-time systems with energy constraints. In: 2009 Third International Conference on Digital Society. Cancun: IEEE: 2009. p. 266\u201371."},{"key":"132_CR55","unstructured":"Lucio L, Mustafiz S, Denil J, Meyers B, Vangheluwe H. The formalism transformation graph as a guide to model driven engineering. McGill University, Tech. Rep. SOCS-TR2012. 2012."},{"key":"132_CR56","unstructured":"Lucio L, Denil J, Vangheluwe H. An overview of model transformations for a simple automotive power window. Technical report, McGill University, Tech. Rep. SOCS-TR-2012.2, 2012, http:\/\/msdl.cs.mcgill~.... 2012."},{"key":"132_CR57","doi-asserted-by":"crossref","unstructured":"Moln\u00e1r V, Graics B, V\u00f6r\u00f6s A, Majzik I, Varr\u00f3 D. The gamma statechart composition framework: Design, verification and code generation for component-based reactive systems. In: 2018 IEEE\/ACM 40th International Conference on Software Engineering: Companion (ICSE-Companion). IEEE: 2018. p. 113\u20136.","DOI":"10.1145\/3183440.3183489"},{"key":"132_CR58","volume-title":"International Workshop on Design, Modeling, and Evaluation of Cyber Physical Systems","author":"W Ahmad","year":"2016","unstructured":"Ahmad W, Yildiz BM, Rensink A, Stoelinga M. A model-driven framework for hardware-software co-design of dataflow applications. In: International Workshop on Design, Modeling, and Evaluation of Cyber Physical Systems. Pittsburgh: Springer: 2016. p. 1\u201316."},{"key":"132_CR59","unstructured":"Gilliam DP, Powell JD, Bishop M. Application of lightweight formal methods to software security. In: 14th IEEE International Workshops on Enabling Technologies: Infrastructure for Collaborative Enterprise (WETICE\u201905): 2005. p. 160\u20135."},{"key":"132_CR60","volume-title":"Formal Methods and Software Engineering","author":"S Souaf","year":"2019","unstructured":"Souaf S, Loulergue F. A first step in the translation of alloy to coq In: Ait-Ameur Y, Qin S, editors. Formal Methods and Software Engineering. Cham: Springer: 2019. p. 455\u201369."},{"key":"132_CR61","doi-asserted-by":"crossref","unstructured":"Schlingloff H, Kruse PM, Saadatmand M. Excellence in variant testing. In: Proceedings of the 14th International Working Conference on Variability Modelling of Software-Intensive Systems: 2020. p. 1\u20132.","DOI":"10.1145\/3377024.3377028"}],"container-title":["Journal of Internet Services and Applications"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1186\/s13174-021-00132-z.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1186\/s13174-021-00132-z\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1186\/s13174-021-00132-z.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,2,9]],"date-time":"2022-02-09T22:15:32Z","timestamp":1644444932000},"score":1,"resource":{"primary":{"URL":"https:\/\/jisajournal.springeropen.com\/articles\/10.1186\/s13174-021-00132-z"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,5,24]]},"references-count":61,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2021,12]]}},"alternative-id":["132"],"URL":"https:\/\/doi.org\/10.1186\/s13174-021-00132-z","relation":{},"ISSN":["1867-4828","1869-0238"],"issn-type":[{"type":"print","value":"1867-4828"},{"type":"electronic","value":"1869-0238"}],"subject":[],"published":{"date-parts":[[2021,5,24]]},"assertion":[{"value":"21 October 2019","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"3 March 2021","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"24 May 2021","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"The authors declare that they have no competing interests.","order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Competing interests"}}],"article-number":"2"}}