基于Input/Output约束元自动机的系统安全需求建模
Modeling System Safety Requirements Using Input/Output Constraint Meta-Automata
摘要:
最近的软件相关事故是系统事故。为了验证不存在与功能失调的交互有关的系统危害,工业界呼吁对系统安全要求和组件之间以及与环境的交互约束进行建模的方法(例如,人与机器之间)。本文提出了一种基于输入/输出约束元自动机的框架,在Meta层次上对系统行为进行约束。这种方法可以形式化地对系统与其环境之间或其组件之间的安全交互进行建模。该框架不同于传统的模型检验框架。它明确地分离了产品工程师和安全工程师的任务,并提供了一种自顶向下的技术,用于对具有安全约束的系统进行建模,并自动组成符合安全要求的安全系统。这项工作的贡献包括正式系统的安全需求和自动确保系统安全的方式。
英文摘要:
Most recent software related accidents have been system accidents. To validate the absence of system hazards concerning dysfunctional interactions, industrials call for approaches of modeling system safety requirements and interaction constraints among components and with environments (e.g., between humans and machines). This paper proposes a framework based on input/output constraint meta-automata, which restricts system behavior at the meta level. This approach can formally model safe interactions between a system and its environment or among its components. This framework differs from the framework of the traditional model checking. It explicitly separates the tasks of product engineers and safety engineers, and provides a top-down technique for modeling a system with safety constraints, and for automatically composing a safe system that conforms to safety requirements. The contributions of this work include formalizing system safety requirements and a way of automatically ensuring system safety.
机构、总结、中文摘要均由AI分析而来,可能存在错误,请以论文正文为准。