{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,16]],"date-time":"2026-06-16T23:06:09Z","timestamp":1781651169059,"version":"3.54.5"},"reference-count":35,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2024,3,12]],"date-time":"2024-03-12T00:00:00Z","timestamp":1710201600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2024,3,12]],"date-time":"2024-03-12T00:00:00Z","timestamp":1710201600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Innovations Syst Softw Eng"],"published-print":{"date-parts":[[2025,6]]},"abstract":"<jats:title>Abstract<\/jats:title>\n                  <jats:p>\n                    Safety and security are key considerations in the design of critical systems. Requirements analysis methods rely on the expertise and experience of human intervention to make critical judgements. While human judgement is essential to an analysis method, it is also important to ensure a degree of formality so that we\n                    <jats:italic>reason about<\/jats:italic>\n                    safety and security at early stages of analysis and design, rather than detect problems later. In this paper, we present a hierarchical and incremental analysis process that aims to justify the design and flow-down of derived critical requirements arising from safety hazards and security vulnerabilities identified at the system level. The safety and security analysis at each level uses STPA-style action analysis to identify hazards and vulnerabilities. At each level, we verify that the design achieves the safety or security requirements by backing the analysis with formal modelling and proof using Event-B refinement. The formal model helps to identify hazards\/vulnerabilities arising from the design and how they relate to the safety accidents\/security losses being considered at this level. We then re-apply the same process to each component of the design in a hierarchical manner. Thus, we use hazard and vulnerability analysis, together with refinement-based formal modelling and verification, to drive the design, replacing the system level requirements with component requirements. In doing so, we decompose critical system-level requirements down to component-level requirements, transforming them from abstract system level requirements, towards concrete solutions that we can implement correctly so that the hazards\/vulnerabilities are mitigated.\n                  <\/jats:p>","DOI":"10.1007\/s11334-024-00551-8","type":"journal-article","created":{"date-parts":[[2024,3,12]],"date-time":"2024-03-12T19:02:35Z","timestamp":1710270155000},"page":"569-593","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":8,"title":["Systematic hierarchical analysis of requirements for critical systems"],"prefix":"10.1007","volume":"21","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-0508-3066","authenticated-orcid":false,"given":"Asieh Salehi","family":"Fathabadi","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0210-0983","authenticated-orcid":false,"given":"Colin","family":"Snook","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Dana","family":"Dghaym","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4095-0732","authenticated-orcid":false,"given":"Thai Son","family":"Hoang","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Fahad","family":"Alotaibi","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4642-5373","authenticated-orcid":false,"given":"Michael","family":"Butler","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2024,3,12]]},"reference":[{"key":"551_CR1","unstructured":"Eurocae (2014) ED-202A\u2014Airworthiness Security Process Specification. https:\/\/eshop.eurocae.net\/eurocae-documents-and-reports\/ed-202a\/"},{"key":"551_CR2","unstructured":"Eurocae (2018) ED-203A\u2014Airworthiness Security Methods and Considerations. https:\/\/eshop.eurocae.net\/eurocae-documents-and-reports\/ed-203a\/"},{"key":"551_CR3","unstructured":"Leveson NG, Thomas JP (2018) STPA handbook. Cambridge"},{"issue":"2","key":"551_CR4","doi-asserted-by":"publisher","first-page":"31","DOI":"10.1145\/2556938","volume":"57","author":"W Young","year":"2014","unstructured":"Young W, Leveson NG (2014) Inside risks an integrated approach to safety and security based on systems theory: applying a more powerful new safety methodology to security risks. Commun ACM 57(2):31\u201335","journal-title":"Commun ACM"},{"key":"551_CR5","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781139195881","volume-title":"Modeling in event-B: system and software engineering","author":"J-R Abrial","year":"2010","unstructured":"Abrial J-R (2010) Modeling in event-B: system and software engineering. Cambridge University Press, Cambridge"},{"key":"551_CR6","unstructured":"Colley J, Butler M (2013) A formal, systematic approach to STPA using event-B refinement and proof. In: 21th safety critical system symposium"},{"key":"551_CR7","doi-asserted-by":"crossref","unstructured":"Howard G, Butler MJ, Colley J, Sassone V (2017) Formal analysis of safety and security requirements of critical systems supported by an extended STPA methodology. In: 2017 IEEE European symposium on security and privacy workshops","DOI":"10.1109\/EuroSPW.2017.68"},{"issue":"1\u20132","key":"551_CR8","doi-asserted-by":"publisher","first-page":"56","DOI":"10.1504\/IJCCBS.2019.098815","volume":"9","author":"G Howard","year":"2019","unstructured":"Howard G, Butler MJ, Colley J, Sassone V (2019) A methodology for assuring the safety and security of critical infrastructure based on STPA and Event-B. Int J Crit Comput Based Syst 9(1\u20132):56\u201375","journal-title":"Int J Crit Comput Based Syst"},{"key":"551_CR9","volume-title":"Database and expert systems applications","author":"T Omitola","year":"2019","unstructured":"Omitola T, Rezazadeh A, Butler M (2019) Making (implicit) security requirements explicit for cyber-physical systems: a maritime use case security analysis. Database and expert systems applications. Springer, Berlin"},{"key":"551_CR10","unstructured":"Fathabadi S, Snook C, Dghaym D, Hoang TS, Alotaibi F, Butler M (2023) Designing critical systems using hierarchical STPA and Event-B. In: ABZ 2023: rigorous state-based methods"},{"key":"551_CR11","unstructured":"Praxis: Tokeneer. https:\/\/www.adacore.com\/tokeneer. Accessed May 2020"},{"issue":"1","key":"551_CR12","doi-asserted-by":"publisher","first-page":"11","DOI":"10.1109\/TDSC.2004.2","volume":"1","author":"A Avizienis","year":"2004","unstructured":"Avizienis A, Laprie J, Randell B, Landwehr C (2004) Basic concepts and taxonomy of dependable and secure computing. IEEE Trans Depend Secure Comput 1(1):11\u201333","journal-title":"IEEE Trans Depend Secure Comput"},{"issue":"6","key":"551_CR13","first-page":"447","volume":"12","author":"J-R Abrial","year":"2010","unstructured":"Abrial J-R, Butler M, Hallerstede S, Hoang TS, Mehta F, Voisin L (2010) Rodin: an open toolset for modelling and reasoning in Event-B. Softw Tools Technol Transf 12(6):447\u2013466","journal-title":"Softw Tools Technol Transf"},{"issue":"2","key":"551_CR14","first-page":"185","volume":"10","author":"M Leuschel","year":"2008","unstructured":"Leuschel M, Butler M (2008) ProB: an automated analysis toolset for the B method. Softw Tools Technol Transf (STTT) 10(2):185\u2013203","journal-title":"Softw Tools Technol Transf (STTT)"},{"key":"551_CR15","doi-asserted-by":"crossref","unstructured":"Snook C, Hoang TS, Dghaym D, Fathabadi AS, Butler M (2020) Domain-specific scenarios for refinement-based methods. J Syst Archit","DOI":"10.1016\/j.sysarc.2020.101833"},{"key":"551_CR16","unstructured":"Barnes J, Chapman R, Johnson R, Widmaier J, Cooper D, Everett B (2006) Engineering the Tokeneer enclave protection software. In: Proceedings of IEEE international symposium on secure software engineering"},{"key":"551_CR17","unstructured":"Spivey JM (1989) The Z notation\u2014a reference manual. Prentice Hall International Series in Computer Science"},{"key":"551_CR18","doi-asserted-by":"crossref","unstructured":"Rivera V, Bhattacharya S, Cata\u00f1o N (2016) Undertaking the tokeneer challenge in event-B. In: Proceedings of the 4th FME workshop on formal methods in software engineering, FormaliSE@ICSE 2016. ACM","DOI":"10.1145\/2897667.2897671"},{"key":"551_CR19","doi-asserted-by":"publisher","first-page":"855","DOI":"10.1007\/s00165-021-00537-4","volume":"33","author":"S Foster","year":"2021","unstructured":"Foster S, Nemouchi Y, Gleirscher M, Wei R, Kelly T (2021) Integration of formal proof into unified assurance cases with Isabelle\/SACM. Formal Aspects Comput 33:855\u2013884","journal-title":"Formal Aspects Comput"},{"key":"551_CR20","doi-asserted-by":"crossref","unstructured":"Young W, Leveson NG (2013) Systems thinking for safety and security. In: Annual computer security applications conference, ACSAC \u201913. ACM","DOI":"10.1145\/2523649.2530277"},{"key":"551_CR21","first-page":"183","volume":"34","author":"I Friedberg","year":"2017","unstructured":"Friedberg I, McLaughlin K, Smith P, Laverty DM, Sezer S (2017) STPA-SafeSec: safety and security analysis for cyber-physical systems. J Inf Secur Appl 34:183\u2013196","journal-title":"J Inf Secur Appl"},{"key":"551_CR22","doi-asserted-by":"crossref","unstructured":"Pereira DP, Hirata CM, Pagliares R, Nadjm-Tehrani S (2017) Towards combined safety and security constraints analysis. In: Computer safety, reliability, and security\u2014SAFECOMP 2017 workshops, ASSURE, DECSoS, SASSUR, TELERISE, and TIPS. Springer","DOI":"10.1007\/978-3-319-66284-8_7"},{"key":"551_CR23","unstructured":"Blank RM, Secretary A (2011) Guide for conducting risk assessments"},{"key":"551_CR24","unstructured":"Group J.T.F.T.I.I.W (2012) SP 800\u201330 revision 1: guide for conducting risk assessments. Technical report, National Institute of Standards & Technology"},{"key":"551_CR25","doi-asserted-by":"publisher","first-page":"105139","DOI":"10.1016\/j.ssci.2020.105139","volume":"136","author":"D Dghaym","year":"2021","unstructured":"Dghaym D, Hoang TS, Turnock SR, Butler M, Downes J, Pritchard B (2021) An STPA-based formal composition framework for trustworthy autonomous maritime systems. Saf Sci 136:105139","journal-title":"Saf Sci"},{"key":"551_CR26","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1016\/j.proeng.2015.11.498","volume":"128","author":"A Abdulkhaleq","year":"2015","unstructured":"Abdulkhaleq A, Wagner S, Leveson N (2015) A comprehensive safety engineering approach for software-intensive systems based on STPA. Procedia Eng 128:2\u201311","journal-title":"Procedia Eng"},{"key":"551_CR27","doi-asserted-by":"crossref","unstructured":"Hata A, Araki K, Kusakabe S, Omori Y, Lin H (2015) Using hazard analysis stamp\/STPA in developing model-oriented formal specification toward reliable cloud service. In: 2015 international conference on platform technology and service","DOI":"10.1109\/PlatCon.2015.14"},{"key":"551_CR28","unstructured":"Thomas J, Leveson N (2013) Generating formal model-based safety requirements for complex, software-and human-intensive systems. In: Proceedings of the twenty-first safety-critical systems symposium, Bristol, UK"},{"key":"551_CR29","doi-asserted-by":"publisher","first-page":"72814","DOI":"10.1109\/ACCESS.2020.2987972","volume":"8","author":"ASA Hadad","year":"2020","unstructured":"Hadad ASA, Ma C, Ahmed AAO (2020) Formal verification of AADL models by event-B. IEEE Access 8:72814\u201372834","journal-title":"IEEE Access"},{"key":"551_CR30","doi-asserted-by":"publisher","unstructured":"Thorburn R, Sassone V, Fathabadi AS, Aniello L, Butler MJ, Dghaym D, Hoang TS (2022) A lightweight approach to the concurrent use and integration of SYSML and formal methods in systems design. In: K\u00fchn T, Sousa V (eds) Proceedings of the 25th international conference on model driven engineering languages and systems: companion proceedings, MODELS 2022, Montreal, Quebec, Canada, 23\u201328 Oct, 2022, pp 83\u201384. https:\/\/doi.org\/10.1145\/3550356.3559577","DOI":"10.1145\/3550356.3559577"},{"key":"551_CR31","doi-asserted-by":"crossref","unstructured":"Seo J, Kwak J, Kim S (2023) Formally verified software update management system in automotive. In: Symposium on vehicles security and privacy (VehicleSec) 2023","DOI":"10.14722\/vehiclesec.2023.23087"},{"key":"551_CR32","doi-asserted-by":"publisher","DOI":"10.1016\/j.infsof.2015.01.001","author":"Y Prokhorova","year":"2015","unstructured":"Prokhorova Y, Laibinis L, Troubitsyna E (2015) Facilitating construction of safety cases from formal models in event-B. Inf Softw Technol. https:\/\/doi.org\/10.1016\/j.infsof.2015.01.001","journal-title":"Inf Softw Technol"},{"key":"551_CR33","doi-asserted-by":"crossref","unstructured":"Basin DA, Radomirovic S, Schmid L (2016) Modeling human errors in security protocols. In: IEEE 29th computer security foundations symposium","DOI":"10.1109\/CSF.2016.30"},{"issue":"2","key":"551_CR34","doi-asserted-by":"publisher","first-page":"199","DOI":"10.1002\/spe.1002","volume":"41","author":"R Silva","year":"2011","unstructured":"Silva R, Pascal C, Hoang TS, Butler MJ (2011) Decomposition tool for Event-B. Softw Pract Exp 41(2):199\u2013208","journal-title":"Softw Pract Exp"},{"key":"551_CR35","doi-asserted-by":"publisher","unstructured":"Hoang TS, Dghaym D, Snook CF, Butler MJ (2017) A composition mechanism for refinement-based methods. In: 22nd international conference on engineering of complex computer systems, ICECCS 2017, Fukuoka, Japan, 5\u20138 Nov, 2017, pp 100\u2013109 . https:\/\/doi.org\/10.1109\/ICECCS.2017.27","DOI":"10.1109\/ICECCS.2017.27"}],"container-title":["Innovations in Systems and Software Engineering"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s11334-024-00551-8.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s11334-024-00551-8\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s11334-024-00551-8.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T15:02:14Z","timestamp":1750345334000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s11334-024-00551-8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,3,12]]},"references-count":35,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2025,6]]}},"alternative-id":["551"],"URL":"https:\/\/doi.org\/10.1007\/s11334-024-00551-8","relation":{"has-preprint":[{"id-type":"doi","id":"10.21203\/rs.3.rs-3384844\/v1","asserted-by":"object"}]},"ISSN":["1614-5046","1614-5054"],"issn-type":[{"value":"1614-5046","type":"print"},{"value":"1614-5054","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,3,12]]},"assertion":[{"value":"25 September 2023","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"2 February 2024","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"12 March 2024","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}