000106601 001__ 106601
000106601 005__ 20230519145349.0
000106601 0247_ $$2doi$$a10.1016/j.jss.2020.110746
000106601 0248_ $$2sideral$$a119637
000106601 037__ $$aART-2021-119637
000106601 041__ $$aeng
000106601 100__ $$0(orcid)0000-0002-2605-6243$$aBernardi, S.$$uUniversidad de Zaragoza
000106601 245__ $$aSecurity modelling and formal verification of survivability properties: Application to cyber–physical systems
000106601 260__ $$c2021
000106601 5060_ $$aAccess copy available to the general public$$fUnrestricted
000106601 5203_ $$aThe 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.
000106601 536__ $$9info:eu-repo/grantAgreement/ES/MICIU/Medrese-RTI2018-098543-B-I00
000106601 540__ $$9info:eu-repo/semantics/openAccess$$aby-nc-nd$$uhttp://creativecommons.org/licenses/by-nc-nd/3.0/es/
000106601 590__ $$a3.514$$b2021
000106601 591__ $$aCOMPUTER SCIENCE, THEORY & METHODS$$b30 / 111 = 0.27$$c2021$$dQ2$$eT1
000106601 591__ $$aCOMPUTER SCIENCE, SOFTWARE ENGINEERING$$b29 / 110 = 0.264$$c2021$$dQ2$$eT1
000106601 594__ $$a8.9$$b2021
000106601 592__ $$a1.418$$b2021
000106601 593__ $$aInformation Systems$$c2021$$dQ1
000106601 593__ $$aHardware and Architecture$$c2021$$dQ1
000106601 655_4 $$ainfo:eu-repo/semantics/article$$vinfo:eu-repo/semantics/acceptedVersion
000106601 700__ $$aGentile, U.
000106601 700__ $$aMarrone, S.
000106601 700__ $$0(orcid)0000-0002-8917-6584$$aMerseguer, J.$$uUniversidad de Zaragoza
000106601 700__ $$aNardone, R.
000106601 7102_ $$15007$$2570$$aUniversidad de Zaragoza$$bDpto. Informát.Ingenie.Sistms.$$cÁrea Lenguajes y Sistemas Inf.
000106601 773__ $$g171, 110746 (2021), [26 pp]$$pJ. syst. softw.$$tJOURNAL OF SYSTEMS AND SOFTWARE$$x0164-1212
000106601 8564_ $$s1246504$$uhttps://zaguan.unizar.es/record/106601/files/texto_completo.pdf$$yPostprint
000106601 8564_ $$s3004649$$uhttps://zaguan.unizar.es/record/106601/files/texto_completo.jpg?subformat=icon$$xicon$$yPostprint
000106601 909CO $$ooai:zaguan.unizar.es:106601$$particulos$$pdriver
000106601 951__ $$a2023-05-18-13:24:38
000106601 980__ $$aARTICLE