A Clock-Based Framework for Construction of Hybrid Systems

A Clock-Based Framework for Construction of Hybrid Systems
复制标题

DOI:
10.1007/978-3-642-39718-9_2
复制
发表时间:
2013-09
期刊:
--
影响因子:
--
通讯作者:
Jifeng He
Jifeng He
中科院分区:
其他
文献类型:
--
作者:
Jifeng He

文献摘要

被引文献

相似文献

混杂系统是由连续的物理部件和离散的控制部件组成的,其中系统状态按照离散和连续动态的相互作用规律随时间演化。计算和控制的结合会导致非常复杂的系统设计。而不是解决混合动力系统的正式验证,本文forcuses一般建模,旨在建模混合动力学,以这样一种方式,可以提取的控制组件的规格从总系统的规格和期望的行为的物理组件。我们处理更明确的混合模型,提供了一个基于时钟和同步信号的数学框架。本文提出了一个抽象的概念,时钟与两个合适的度量空间的时间顺序和时间延迟的描述,并链接时钟与同步事件,显示如何表示的事件发生的时钟。我们通过给离散变量一个基于时钟的表示来处理它们,并展示如何通过记录特定类型变化发生的时刻来捕获连续组件的动态行为。本文介绍了一种基于时钟的离散和连续动力学描述和推理的混合语言,并将其应用于一类物理设备,演示了如何基于时钟来指定一个水罐车并构造和验证其控制器。
Hybrid systems are composed by continuous physical component and discrete control component where the system state evolves over time according to interacting law of discrete and continuous dynamics. Combinations of computation and control can lead to very complicated system designs. Rather than address the formal verification of hybrid systems, this paper forcuses on general modelers, aimed at modelling hybrid dynamics in such a way one can extract the specification of the control component from the specification of the total system and the desire behaviour of the physical component. We treat more explicit hybrid models by providing a mathematical framework based on clock and synchronous signal. This paper presents an abstract concept ofclockwith two suitable metric spaces for description of temporal order and time latency, and links clocks with synchronous events by showing how to represent the occurrences of an event by a clock. We tackle discrete variables by giving them a clock-based representation, and show how to capture dynamical behaviours of continuous components by recording the time instants when a specific type of changes take place. This paper introduces a clock-based hybrid language for description and reasoning of both discrete and continuous dynamics, and applies it to a family of physical devices, and demonstrates how to specify a water tanker and construct and verify its controller based on clocks.