106601 20230519145349.0 doi 10.1016/j.jss.2020.110746 sideral 119637 ART-2021-119637 eng Bernardi, S. Universidad de Zaragoza (orcid)0000-0002-2605-6243 Security modelling and formal verification of survivability properties: Application to cyber–physical systems 2021 Access copy available to the general public Unrestricted The modelling and verification of systems security is an open research topic whose complexity and importance needs, in our view, the use of formal and non-formal methods. This paper addresses the modelling of security using misuse cases and the automatic verification of survivability properties using model checking. The survivability of a system characterises its capacity to fulfil its mission (promptly) in the presence of attacks, failures, or accidents, as defined by Ellison. The original contributions of this paper are a methodology and its tool support, through a framework called surreal. The methodology starts from a misuse case specification enriched with UML profile annotations and obtains, as a by-product, a survivability assessment model (SAM). Using predefined queries the survivability properties are proved in the SAM. A total of fourteen properties have been formulated and also implemented in surreal, which encompasses tools to model the security specification, to create the SAM and to prove the properties. Finally, the paper validates the methodology and the framework using a cyber–physical system (CPS) case study, in the automotive field. info:eu-repo/grantAgreement/ES/MICIU/Medrese-RTI2018-098543-B-I00 info:eu-repo/semantics/openAccess by-nc-nd http://creativecommons.org/licenses/by-nc-nd/3.0/es/ 3.514 2021 COMPUTER SCIENCE, THEORY & METHODS 30 / 111 = 0.27 2021 Q2 T1 COMPUTER SCIENCE, SOFTWARE ENGINEERING 29 / 110 = 0.264 2021 Q2 T1 1.418 2021 Information Systems 2021 Q1 Hardware and Architecture 2021 Q1 8.9 2021 info:eu-repo/semantics/article info:eu-repo/semantics/acceptedVersion Gentile, U. Marrone, S. Merseguer, J. Universidad de Zaragoza (orcid)0000-0002-8917-6584 Nardone, R. 5007 570 Universidad de Zaragoza Dpto. Informát.Ingenie.Sistms. Área Lenguajes y Sistemas Inf. 171, 110746 (2021), [26 pp] J. syst. softw. JOURNAL OF SYSTEMS AND SOFTWARE 0164-1212 1246504 http://zaguan.unizar.es/record/106601/files/texto_completo.pdf Postprint 3004649 http://zaguan.unizar.es/record/106601/files/texto_completo.jpg?subformat=icon icon Postprint oai:zaguan.unizar.es:106601 articulos driver 2023-05-18-13:24:38 ARTICLE