Rigorous State-Based Methods - 9th International Conference, ABZ 2023, Nancy, France, May 30-June 2, 2023, Proceedings
Rigorous State-Based Methods - 9th International Conference, ABZ 2023, Nancy, France, May 30-June 2, 2023, Proceedings
复制标题
严格的基于国家的方法 - 第九届国际会议，ABZ 2023，法国南锡，2023 年 5 月 30 日至 6 月 2 日，会议记录
DOI：
10.1007/978-3-031-33163-3_17
复制
发表时间：
2023
期刊：
影响因子：
--
通讯作者：
Salehi Fathabadi A
中科院分区：
文献类型：
--
作者：
Salehi Fathabadi A
在关键系统的设计中，确保一定程度的正式性非常重要，以便我们在分析和设计的早期阶段就安全性和安保进行推理，而不是事后才发现问题。受 STPA 思想的影响，我们提出了一个分层分析过程，旨在证明因系统级别识别的安全隐患和安全漏洞而产生的派生关键要求的设计和流程的合理性。在每个级别，我们都会通过使用事件 B 细化的正式建模和证明来支持分析，从而验证设计是否达到了安全/安保要求。正式模型有助于识别设计中产生的危险/漏洞以及它们与该级别考虑的安全事故/安全损失的关系。然后，我们以分层方式将相同的过程重新应用于设计的每个组件。因此，我们使用由 Event-B 模型支持的 STPA 思想来驱动设计，用组件需求取代系统级需求。在此过程中，我们将关键需求分解为组件，将它们从抽象的系统级需求转变为我们可以正确实施的具体解决方案，从而消除危险/漏洞。
In the design of critical systems, it is important to ensure a degree of formality so that we reason about safety and security at early stages of analysis and design, rather than detect problems later. Influenced by ideas from STPA we present a hierarchical 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. At each level, we verify that the design achieves the safety/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 ideas from STPA, backed by Event-B models, to drive the design, replacing the system level requirements with component requirements. In doing so, we decompose critical requirements down to components, transforming them from abstract system level requirements, towards concrete solutions that we can implement correctly so that the hazards/vulnerabilities are eliminated.