{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,8,25]],"date-time":"2024-08-25T11:28:41Z","timestamp":1724585321245},"reference-count":72,"publisher":"Elsevier BV","license":[{"start":{"date-parts":[[2021,1,1]],"date-time":"2021-01-01T00:00:00Z","timestamp":1609459200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"}],"funder":[{"name":"Spanish Ministry of Science, Innovation and Universities","award":["Medrese-RTI2018-098543-B-I00"]}],"content-domain":{"domain":["elsevier.com","sciencedirect.com"],"crossmark-restriction":true},"short-container-title":["Journal of Systems and Software"],"published-print":{"date-parts":[[2021,1]]},"DOI":"10.1016\/j.jss.2020.110746","type":"journal-article","created":{"date-parts":[[2020,7,18]],"date-time":"2020-07-18T01:31:42Z","timestamp":1595035902000},"page":"110746","update-policy":"http:\/\/dx.doi.org\/10.1016\/elsevier_cm_policy","source":"Crossref","is-referenced-by-count":17,"special_numbering":"C","title":["Security modelling and formal verification of survivability properties: Application to cyber\u2013physical systems"],"prefix":"10.1016","volume":"171","author":[{"given":"S.","family":"Bernardi","sequence":"first","affiliation":[]},{"given":"U.","family":"Gentile","sequence":"additional","affiliation":[]},{"given":"S.","family":"Marrone","sequence":"additional","affiliation":[]},{"given":"J.","family":"Merseguer","sequence":"additional","affiliation":[]},{"given":"R.","family":"Nardone","sequence":"additional","affiliation":[]}],"member":"78","reference":[{"key":"10.1016\/j.jss.2020.110746_b1","doi-asserted-by":"crossref","first-page":"58","DOI":"10.1109\/MS.2003.1159030","article-title":"Misuse cases: use cases with hostile intent","volume":"20","author":"Alexander","year":"2003","journal-title":"IEEE Softw."},{"key":"10.1016\/j.jss.2020.110746_b2","doi-asserted-by":"crossref","first-page":"361","DOI":"10.1109\/TSE.2012.41","article-title":"Elaborating requirements using model checking and inductive learning","volume":"39","author":"Alrajeh","year":"2013","journal-title":"IEEE Trans. Softw. Eng."},{"key":"10.1016\/j.jss.2020.110746_b3","series-title":"Uncertainty Modeling and Analysis in Engineering and the Sciences","author":"Ayyub","year":"2006"},{"key":"10.1016\/j.jss.2020.110746_b4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"369","DOI":"10.1007\/3-540-48119-2_22","article-title":"M\u00e9t\u00e9or: A successful application of B in a large project","volume":"vol. 1708","author":"Behm","year":"1999"},{"key":"10.1016\/j.jss.2020.110746_b5","doi-asserted-by":"crossref","first-page":"116","DOI":"10.1016\/j.scico.2016.09.002","article-title":"Dynamic state machines for modelling railway control systems","volume":"133","author":"Benerecetti","year":"2017","journal-title":"Sci. Comput. Program."},{"key":"10.1016\/j.jss.2020.110746_b6","first-page":"485","article-title":"A model-driven approach to survivability requirement assessment for critical systems","volume":"230","author":"Bernardi","year":"2016","journal-title":"Proc. Inst. Mech. Eng. Part O: J. Risk Reliab."},{"key":"10.1016\/j.jss.2020.110746_b7","series-title":"Model-Driven Dependability Assessment of Software Systems","author":"Bernardi","year":"2013"},{"key":"10.1016\/j.jss.2020.110746_b8","first-page":"19:1","article-title":"Model-based quantitative evaluation of repair procedures in gas distribution networks","volume":"3","author":"Biagi","year":"2018","journal-title":"ACM Trans. Cyber-Phys. Syst."},{"key":"10.1016\/j.jss.2020.110746_b9","doi-asserted-by":"crossref","first-page":"117","DOI":"10.1016\/S0065-2458(03)58003-2","article-title":"Bounded model checking","volume":"58","author":"Biere","year":"2003","journal-title":"Adv. Comput."},{"key":"10.1016\/j.jss.2020.110746_b10","doi-asserted-by":"crossref","first-page":"147","DOI":"10.1007\/s10270-014-0400-x","article-title":"A profile and tool for modelling safety information with design information in SysML","volume":"15","author":"Biggs","year":"2016","journal-title":"Softw. Syst. Model."},{"key":"10.1016\/j.jss.2020.110746_b11","doi-asserted-by":"crossref","first-page":"19","DOI":"10.1145\/3089649.3089656","article-title":"Software engineering for smart cyber-physical systems: Challenges and promising solutions","volume":"42","author":"Bures","year":"2017","journal-title":"SIGSOFT Softw. Eng. Notes"},{"key":"10.1016\/j.jss.2020.110746_b12","series-title":"Large-Scale Complex IT Systems. Development, Operation and Management","first-page":"303","article-title":"Compositional reverification of probabilistic safety properties for large-scale complex it systems","author":"Calinescu","year":"2012"},{"key":"10.1016\/j.jss.2020.110746_b13","series-title":"CENELEC EN 50128 Railway Applications - Communication, Signalling and Processing Systems - Software for Railway Control and Protection Systems","author":"CENELEC","year":"2011"},{"key":"10.1016\/j.jss.2020.110746_b14","series-title":"Future of Software Engineering (FOSE\u201907)","first-page":"285","article-title":"Research directions in requirements engineering","author":"Cheng","year":"2007"},{"key":"10.1016\/j.jss.2020.110746_b15","doi-asserted-by":"crossref","first-page":"359","DOI":"10.1007\/3-540-45657-0_29","article-title":"NuSMV 2: An open source tool for symbolic model checking","volume":"2404","author":"Cimatti","year":"2002","journal-title":"Lecture Notes in Comput. Sci."},{"key":"10.1016\/j.jss.2020.110746_b16","article-title":"Eliciting efficiency requirements with use cases","volume":"3","author":"D\u00f6rr","year":"2003"},{"key":"10.1016\/j.jss.2020.110746_b17","doi-asserted-by":"crossref","first-page":"523","DOI":"10.1007\/s10270-016-0572-7","article-title":"A model-driven approach for vulnerability evaluation of modern physical protection systems","volume":"18","author":"Drago","year":"2019","journal-title":"Softw. Syst. Model."},{"key":"10.1016\/j.jss.2020.110746_b18","doi-asserted-by":"crossref","first-page":"68782","DOI":"10.1109\/ACCESS.2018.2873328","article-title":"Network foundation for command and control (c2) systems: Literature review","volume":"6","author":"Eisenberg","year":"2018","journal-title":"IEEE Access"},{"key":"10.1016\/j.jss.2020.110746_b19","doi-asserted-by":"crossref","first-page":"70","DOI":"10.1109\/52.776952","article-title":"Survivable network system analysis: A case study","volume":"16","author":"Ellison","year":"1999","journal-title":"IEEE Softw."},{"key":"10.1016\/j.jss.2020.110746_b20","series-title":"Computer Aided Verification","first-page":"454","article-title":"Combining model learning and model checking to analyze TCP implementations","author":"Fiter\u0103u-Bro\u015ftean","year":"2016"},{"key":"10.1016\/j.jss.2020.110746_b21","first-page":"183","article-title":"Stpa-safesec: Safety and security analysis for cyber-physical systems","volume":"34","author":"Friedberg","year":"2017","journal-title":"J. Inf. Secur. Appl."},{"key":"10.1016\/j.jss.2020.110746_b22","series-title":"A Practical Guide to SysML: Systems Modeling Language","author":"Friedenthal","year":"2008"},{"key":"10.1016\/j.jss.2020.110746_b23","unstructured":"Fuxman, A., Pistore, M., Mylopoulos, J., Traverso, P., 2001. Model checking early requirements specifications in Tropos. In: Proceedings Fifth IEEE International Symposium on Requirements Engineering, pp. 174\u2013181."},{"key":"10.1016\/j.jss.2020.110746_b24","doi-asserted-by":"crossref","first-page":"146","DOI":"10.1145\/318774.318939","article-title":"Using model checking to generate tests from requirements specifications","volume":"24","author":"Gargantini","year":"1999","journal-title":"SIGSOFT Softw. Eng. Notes"},{"key":"10.1016\/j.jss.2020.110746_b25","series-title":"Model Checking Software","first-page":"24","article-title":"Minimal counterexample generation for SPIN","author":"Gastin","year":"2007"},{"key":"10.1016\/j.jss.2020.110746_b26","doi-asserted-by":"crossref","first-page":"175","DOI":"10.3233\/JHS-170564","article-title":"A model driven approach for assessing survivability requirements of critical infrastructures","volume":"23","author":"Gentile","year":"2017","journal-title":"J. High Speed Netw."},{"key":"10.1016\/j.jss.2020.110746_b27","doi-asserted-by":"crossref","first-page":"338","DOI":"10.1109\/TSE.2010.36","article-title":"Verification and trade-off analysis of security properties in UML system models","volume":"36","author":"Georg","year":"2010","journal-title":"IEEE Trans. Softw. Eng."},{"key":"10.1016\/j.jss.2020.110746_b28","series-title":"Automated planning: Theory and practice","author":"Ghallab","year":"2004"},{"key":"10.1016\/j.jss.2020.110746_b29","series-title":"19th IEEE International Symposium on High Assurance Systems Engineering, HASE 2019, Hangzhou, China, January (2019) 3-5","first-page":"74","article-title":"Engineering functional safety requirements for automotive systems: A cyber-physical-social approach","author":"Gharib","year":"2019"},{"key":"10.1016\/j.jss.2020.110746_b30","series-title":"AIAA Infotech@Aerospace Conference","article-title":"Software survivability: Where safety and security converge","author":"Goertzel","year":"2009"},{"key":"10.1016\/j.jss.2020.110746_b31","series-title":"Integrating Security and Software Engineering: Advances and Future Visions","first-page":"190","article-title":"An integrated security verification and security solution design trade-off analysis","author":"Houmb","year":"2007"},{"key":"10.1016\/j.jss.2020.110746_b32","series-title":"2017 IEEE European Symposium on Security and Privacy Workshops (EuroS PW)","first-page":"174","article-title":"Formal analysis of safety and security requirements of critical systems supported by an extended stpa methodology","author":"Howard","year":"2017"},{"key":"10.1016\/j.jss.2020.110746_b33","doi-asserted-by":"crossref","first-page":"1802","DOI":"10.1109\/JIOT.2017.2703172","article-title":"Cyber-physical systems security \u2013 a survey","volume":"4","author":"Humayed","year":"2017","journal-title":"IEEE Internet Things J."},{"key":"10.1016\/j.jss.2020.110746_b34","series-title":"IEC 61508: Functional Safety of Electrical\/electronic\/programmable electronic safety-related systems","author":"International Electrotechnical Commission","year":"1998"},{"key":"10.1016\/j.jss.2020.110746_b35","series-title":"Road Vehicles - Functional Safety","year":"2011"},{"key":"10.1016\/j.jss.2020.110746_b36","series-title":"Proceedings of the 5th International Conference on the Unified Modeling Language, UML \u201902","first-page":"412","article-title":"Umlsec: Extending UML for secure systems development","author":"J\u00fcrjens","year":"2002"},{"key":"10.1016\/j.jss.2020.110746_b37","series-title":"Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)","first-page":"414","article-title":"Replacing testing with formal verification in intel\u00ae coretm i7 processor execution engine validation","volume":"vol. 5643","author":"Kaivola","year":"2009"},{"key":"10.1016\/j.jss.2020.110746_b38","series-title":"Architecting Dependable Systems II","first-page":"51","article-title":"Achieving critical system survivability through software architectures","author":"Knight","year":"2004"},{"key":"10.1016\/j.jss.2020.110746_b39","doi-asserted-by":"crossref","first-page":"320","DOI":"10.1016\/j.ress.2008.03.025","article-title":"SMV model-based safety analysis of software requirements","volume":"94","author":"Koh","year":"2009","journal-title":"Reliab. Eng. Syst. Saf."},{"key":"10.1016\/j.jss.2020.110746_b40","article-title":"The real story of stuxnet","author":"Kushnet","year":"2013","journal-title":"IEEE Spectr."},{"key":"10.1016\/j.jss.2020.110746_b41","series-title":"Proc. 23rd International Conference on Computer Aided Verification (CAV\u201911)","first-page":"585","article-title":"PRISM 4.0: Verification of probabilistic real-time systems","volume":"vol. 6806","author":"Kwiatkowska","year":"2011"},{"key":"10.1016\/j.jss.2020.110746_b42","series-title":"22nd IEEE\/ACM International Conference on Automated Software Engineering (ASE 2007)","first-page":"445","article-title":"Improving UML profile design practices by leveraging conceptual domain models","author":"Lagarde","year":"2007"},{"key":"10.1016\/j.jss.2020.110746_b43","series-title":"A Collection of Technical Papers - 1st Space Exploration Conference: Continuing the Voyage of Discovery, Vol. 1","first-page":"584","article-title":"Safety and risk-driven design in complex systems-of-systems","author":"Leveson","year":"2005"},{"key":"10.1016\/j.jss.2020.110746_b44","series-title":"The Unified Modeling Language. UML 2002","article-title":"SecureUML: A UML-based modeling language for model-driven security","volume":"vol. 2460","author":"Lodderstedt","year":"2002"},{"key":"10.1016\/j.jss.2020.110746_b45","doi-asserted-by":"crossref","unstructured":"Lopatkin, I., Iliasov, A., Romanovsky, A., Prokhorova, Y., Troubitsyna, E., 2011. Patterns for representing FMEA in formal specification of control systems. In: Proceedings of IEEE International Symposium on High Assurance Systems Engineering, pp. 146\u2013151.","DOI":"10.1109\/HASE.2011.10"},{"key":"10.1016\/j.jss.2020.110746_b46","series-title":"Foundations of Security Analysis and Design VI","first-page":"231","author":"Lund","year":"2011"},{"key":"10.1016\/j.jss.2020.110746_b47","doi-asserted-by":"crossref","first-page":"275","DOI":"10.1016\/j.compeleceng.2015.07.011","article-title":"On synergies of cyber and physical security modelling in vulnerability assessment of railway systems","volume":"47","author":"Marrone","year":"2015","journal-title":"Comput. Electr. Eng."},{"key":"10.1016\/j.jss.2020.110746_b48","doi-asserted-by":"crossref","DOI":"10.1016\/j.micpro.2016.01.007","article-title":"Component-based design of cyber-physical applications with safety-critical requirements","volume":"42","author":"Masrur","year":"2016","journal-title":"Microprocess. Microsyst."},{"key":"10.1016\/j.jss.2020.110746_b49","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"345","DOI":"10.1007\/978-3-319-21070-4_35","article-title":"Analyzing requirements using environment modelling","volume":"vol. 9185","author":"M\u00e9ry","year":"2015"},{"key":"10.1016\/j.jss.2020.110746_b50","series-title":"Secure Software Systems Engineering: The Secure Tropos Approach (Invited Paper), Vol. 6","author":"Mouratidis","year":"2011"},{"key":"10.1016\/j.jss.2020.110746_b51","series-title":"UML Profile for MARTE: Modeling and Analysis of Real-Time Embedded Systems","year":"2011"},{"key":"10.1016\/j.jss.2020.110746_b52","series-title":"Website","year":"2019"},{"key":"10.1016\/j.jss.2020.110746_b53","series-title":"IS Olympics: Information Systems in a Diverse World","first-page":"95","article-title":"A CASE tool to support automated modelling and analysis of security requirements, based on secure tropos","author":"Pavlidis","year":"2012"},{"key":"10.1016\/j.jss.2020.110746_b54","first-page":"64","article-title":"A survey on security requirement elicitation methods: Classification, merits and demerits","volume":"11","author":"Raja\u00a0Ramesh","year":"2016","journal-title":"Int. J. Appl. Eng. Res."},{"key":"10.1016\/j.jss.2020.110746_b55","article-title":"Modelling security of critical infrastructures: A survivability assessment","author":"Rodr\u00edguez","year":"2014","journal-title":"Comput. J."},{"key":"10.1016\/j.jss.2020.110746_b56","series-title":"2013 3rd International Workshop on Model-Driven Requirements Engineering, MoDRE 2013 - Proceedings","first-page":"55","article-title":"Towards the model-driven engineering of security requirements for embedded systems","author":"Roudier","year":"2013"},{"key":"10.1016\/j.jss.2020.110746_b57","first-page":"193","article-title":"Integration of model-based engineering with system safety analysis","volume":"15","author":"Scholz","year":"2013","journal-title":"Int. J. Ind. Syst. Eng."},{"key":"10.1016\/j.jss.2020.110746_b58","doi-asserted-by":"crossref","first-page":"19","DOI":"10.1109\/MS.2003.1231146","article-title":"The pragmatics of model-driven development","volume":"20","author":"Selic","year":"2003","journal-title":"IEEE Softw."},{"key":"10.1016\/j.jss.2020.110746_b59","series-title":"Tenth IEEE International Symposium on Object-Oriented Real-Time Distributed Computing (ISORC 2007), 7-9 May (2007)","first-page":"2","article-title":"A systematic approach to domain-specific language design using UML","author":"Selic","year":"2007"},{"key":"10.1016\/j.jss.2020.110746_b60","unstructured":"Sheyner, O., Haines, J., Jha, S., Lippmann, R., Wing, J., 2002. Automated generation and analysis of attack graphs. In: Proceedings of the IEEE Computer Society Symposium on Research in Security and Privacy, pp. 273\u2013284."},{"key":"10.1016\/j.jss.2020.110746_b61","series-title":"2019 IEEE 8th Joint International Information Technology and Artificial Intelligence Conference (ITAIC)","first-page":"1143","article-title":"A new software failure analysis method based on the system reliability modeling","author":"Song","year":"2019"},{"key":"10.1016\/j.jss.2020.110746_b62","doi-asserted-by":"crossref","first-page":"3453","DOI":"10.1109\/COMST.2018.2855563","article-title":"A survey of iot-enabled cyberattacks: Assessing attack paths to critical infrastructures and services","volume":"20","author":"Stellios","year":"2018","journal-title":"IEEE Commun. Surv. Tutor."},{"key":"10.1016\/j.jss.2020.110746_b63","series-title":"Website","year":"2019"},{"key":"10.1016\/j.jss.2020.110746_b64","series-title":"Model-Driven Architecture Specification and Standardisation","year":"2018"},{"key":"10.1016\/j.jss.2020.110746_b65","series-title":"3rd International Conference on Systems, ICONS 2008","first-page":"202","article-title":"Elicitation and specification of safety requirements","author":"Troubitsyna","year":"2008"},{"key":"10.1016\/j.jss.2020.110746_b66","series-title":"International Conference on Computer Networks and Information Technology","first-page":"333","article-title":"A survey on issues in non-functional requirements elicitation","author":"Ullah","year":"2011"},{"key":"10.1016\/j.jss.2020.110746_b67","series-title":"Unified Modeling Language: Infrastructure","year":"2017"},{"key":"10.1016\/j.jss.2020.110746_b68","doi-asserted-by":"crossref","first-page":"68","DOI":"10.1016\/j.jss.2016.11.031","article-title":"Integration between requirements engineering and safety analysis: A systematic literature review","volume":"125","author":"Vilela","year":"2017","journal-title":"J. Syst. Softw."},{"key":"10.1016\/j.jss.2020.110746_b69","doi-asserted-by":"crossref","first-page":"143","DOI":"10.1007\/978-3-319-04426-2_8","article-title":"A model-driven process for physical protection system design and vulnerability evaluation","volume":"27","author":"Vittorini","year":"2015","journal-title":"Top. Saf. Risk Reliab. Qual."},{"key":"10.1016\/j.jss.2020.110746_b70","doi-asserted-by":"crossref","first-page":"373","DOI":"10.1016\/j.engfailanal.2019.06.020","article-title":"Avionics system failure analysis and verification based on model checking","volume":"105","author":"Wang","year":"2019","journal-title":"Eng. Fail. Anal."},{"key":"10.1016\/j.jss.2020.110746_b71","doi-asserted-by":"crossref","first-page":"73","DOI":"10.1016\/j.jss.2003.10.018","article-title":"A formal software requirements specification method for digital nuclear plant protection systems","volume":"74","author":"Yoo","year":"2005","journal-title":"J. Syst. Softw."},{"key":"10.1016\/j.jss.2020.110746_b72","article-title":"State of the art of cyber-physical systems security: an automatic control perspective","volume":"149","author":"Zacchia\u00a0Lun","year":"2018","journal-title":"J. Syst. Softw."}],"container-title":["Journal of Systems and Software"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0164121220301710?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0164121220301710?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2021,1,13]],"date-time":"2021-01-13T04:34:43Z","timestamp":1610512483000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S0164121220301710"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,1]]},"references-count":72,"alternative-id":["S0164121220301710"],"URL":"https:\/\/doi.org\/10.1016\/j.jss.2020.110746","relation":{},"ISSN":["0164-1212"],"issn-type":[{"value":"0164-1212","type":"print"}],"subject":[],"published":{"date-parts":[[2021,1]]},"assertion":[{"value":"Elsevier","name":"publisher","label":"This article is maintained by"},{"value":"Security modelling and formal verification of survivability properties: Application to cyber\u2013physical systems","name":"articletitle","label":"Article Title"},{"value":"Journal of Systems and Software","name":"journaltitle","label":"Journal Title"},{"value":"https:\/\/doi.org\/10.1016\/j.jss.2020.110746","name":"articlelink","label":"CrossRef DOI link to publisher maintained version"},{"value":"article","name":"content_type","label":"Content Type"},{"value":"\u00a9 2020 Published by Elsevier Inc.","name":"copyright","label":"Copyright"}],"article-number":"110746"}}