Algebraic calculi for hybrid systems
Algebraic calculi for hybrid systems
复制标题
混合系统的代数演算
DOI：
--
复制
发表时间：
2009
期刊：
影响因子：
--
通讯作者：
P. Höfner
中科院分区：
文献类型：
--
作者：
P. Höfner
在过去的几十年里，不正确的软件已经夺去了许多人的生命，并造成了环境破坏。此外，不正确的软件经常造成经济损失。与环境交互的系统特别容易出错。一方面，它们必须足够灵活，以应对环境变化，另一方面，它们必须是可预测的。与用于操作的软件系统不同，交互系统必须满足严格的安全标准-混合系统经常被用来模拟这样的安全关键系统。它们是异质系统，其特征是连续动态和导致状态变化的离散事件的相互作用。他们已经发现了广泛的应用范围从控制和医疗工程航空电子。但即使是生物和化学过程也可以用这样的系统来简明地描述。在许多情况下，即使使用当今拥有巨大内存和计算能力的计算机，混合系统也过于复杂，无法进行计算机辅助验证。在这本书中，我们的目标是一个紧凑的处理验证任务。代数技术是特别感兴趣的，并以自然的方式出现。系统是用类似于高中时已知的方程组来代数描述的。代数方法的优点是简洁、清晰和简单;特别是在（计算机辅助）计算规则方面。开发的混合动力系统的代数表征允许，例如，通过简单的代数变换验证安全方面。该方法还使得能够使用现成的自动定理证明器。这些证明器可以用来验证混合系统的基本性质。在过去的十年中，几十个基于逻辑的方法已被应用到混合动力系统。这些方法的范围从经典的命题逻辑和模态或时态逻辑，已转移到混合系统的特殊逻辑，已开发的。它们中的大多数都是很好理解的，但由于它们的不同概念，语法和语义没有统一的处理。因此，我们探索一个紧凑的和统一的处理所有这些逻辑。的union是基于相同的代数技术的混合动力系统的特性。这允许通过所有统一的艾德逻辑进行交叉推理。在这本书中，我们特别注意所涉及的逻辑和混合系统之间的关系。这本书提出了基本方法的分析混合动力系统和结果在一个连贯的家庭代数演算的混合动力系统。最后通过实例分析，证明了该理论的适用性和实用性。
Over the past decades incorrect software has claimed numerous lives and has caused environmental damages. Furthermore incorrect software regularly yields economic losses. Systems that interact with their environment are especially fault-prone. On the one hand, they have to be exible enough to react to environment changes, on the other hand they have to be predictable. Unlike software systems for o ce work, interacting systems must satisfy restrictive safety criteria an airbag that in ates too late is unacceptable. Hybrid systems are often used to model such safety critical systems. They are heterogeneous systems characterised by the interaction of continuous dynamics and discrete events that cause state changes. They have found widespread applications ranging from control and medical engineering to avionics. But even biological and chemical processes can concisely be described by such systems. In many cases, hybrid systems are too complex for computer-aided veri cation even with today's computers that o er enormous memory and calculating capacities. In this book, we aim at a compact treatment of veri cation tasks. Algebraic techniques are of particular interest and arise in a natural way. Systems are algebraically described by systems of equations that are similar to those known from high school. Advantages that accrue by an algebraic approach are conciseness, clarity and simplicity; in particular with respect to (computer-aided) calculation rules. The developed algebraic characterisation of hybrid systems allows, for example, the veri cation of safety aspects by simple algebraic transformations. The approach further enables the use of o -the-shelf automated theorem provers. These provers can be employed to verify fundamental properties of hybrid systems. Over the last decade dozens of logic-based approaches have been applied to hybrid systems. These approaches range from classical propositional logics and modal or temporal logics that have been transferred over to hybrid systems to special logics that have been developed for them. Most of them are well-understood, but due to their di erent notions, syntax and semantics a uniform treatment is not available. Therefore we explore a compact and uniform treatment for all these logics. The uni cation is based on the same algebraic techniques as for the characterisation of hybrid systems. This allows cross-reasoning through all uni ed logics. In this book we pay special attention to the relationship between the logics involved and hybrid systems. The book presents fundamental methods for the analysis of hybrid systems and results in a coherent family of algebraic calculi for hybrid systems. The suitability and the relevance of the theory is proved by rst case studies.