混合系统中的拒绝服务安全攻击框架
A Framework for Hybrid Systems with Denial-of-Service Security Attack
AI总结：
本文提出一种形式化框架，用于在混合系统中表达拒绝服务攻击，确保在通信不可靠时系统安全。通过开发验证混合系统安全性的推理系统，并应用于列车控制系统示例。
摘要：
混合系统是离散计算和连续物理演化的结合。此类系统的物理组件引入了安全要求，实现这些要求需要离散控制器的正确监控和控制。然而，由于拒绝服务安全攻击，控制器预期的信息无法接收，导致物理系统可能无法按预期行为。本文提出了一种形式化框架，用于在混合系统中表达拒绝服务安全攻击。作为优点，物理系统能够在理想控制失效时规划合理行为，以确保在拒绝服务情况下的系统安全性。在建模语言的背景下，我们开发了一个推理系统来验证混合系统的安全性，不假设环境行为。基于该推理系统，我们实现了交互式定理证明器，并将其应用于列车控制系统示例的检查。
英文摘要：
Hybrid systems are integrations of discrete computation and continuous physical evolution. The physical components of such systems introduce safety requirements, the achievement of which asks for the correct monitoring and control from the discrete controllers. However, due to denial-of-service security attack, the expected information from the controllers is not received and as a consequence the physical systems may fail to behave as expected. This paper proposes a formal framework for expressing denial-of-service security attack in hybrid systems. As a virtue, a physical system is able to plan for reasonable behavior in case the ideal control fails due to unreliable communication, in such a way that the safety of the system upon denial-of-service is still guaranteed. In the context of the modeling language, we develop an inference system for verifying safety of hybrid systems, without putting any assumptions on how the environments behave. Based on the inference system, we implement an interactive theorem prover and have applied it to check an example taken from train control system.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
