使用控制自动机形式化安全需求
Formalizing Safety Requirements Using Controlling Automata
摘要：
安全性是可靠性的一个重要因素。它被定义为没有事故。大多数涉及软件密集型系统的事故都是系统事故，这是由不安全的系统间或组件间交互引起的。为了验证不存在与功能失调的交互相关的系统危害，工业界呼吁对系统安全需求和组件之间的交互约束进行建模的方法。本文提出了这样一种形式主义，即接口控制系统（或简称C-Systems）。接口C系统由接口自动机和控制自动机组成，在Meta级上形式化安全交互并约束系统行为。该框架不同于传统的模型检验框架。它明确地分离了产品工程师和安全工程师的任务，并提供了一种自顶向下的技术，用于对具有安全约束的系统进行建模，并自动组成符合安全要求的安全系统。这项工作的贡献包括正式的安全要求和自动确保系统安全的方式。
英文摘要：
Safety is an important element of dependability. It is defined as the absence of accidents. Most accidents involving software-intensive systems have been system accidents, which are caused by unsafe inter-system or inter-component interactions. To validate the absence of system hazards concerning dysfunctional interactions, industrials call for approaches of modeling system safety requirements and interaction constraints among components. This paper proposes such a formalism, namely interface control systems (or shortly C-Systems). An interface C-System is composed of an interface automaton and a controlling automaton, which formalizes safe interactions and restricts system behavior at the meta level. This framework differs from the framework of 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 safety requirements and a way of automatically ensuring system safety.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
