Modeling and verification of hybrid systems with clocked and unclocked events
Modeling and verification of hybrid systems with clocked and unclocked events
复制标题
具有时钟和非时钟事件的混合系统的建模和验证
DOI：
10.1109/cdc.2001.980198
复制
发表时间：
2001
期刊：
影响因子：
--
通讯作者：
B. Krogh
中科院分区：
文献类型：
--
作者：
B. I. Silva;B. Krogh
我们定义采样数据混合自动机（SDHA），模型系统的时钟和非时钟事件。虽然时钟事件可以在标准的混合自动机通过引入额外的连续状态变量建模，我们在本文中展示了如何SDHA形式主义提供了一个更有效的计算方法验证的基础。为此，我们定义了一个过渡系统的SDHA语义，并提出了一种方法来计算近似商过渡系统使用现有的工具计算可达集的混合动力系统的修改。通过实例说明了SDHA模型检验过程的定义和要素。
We define sampled-data hybrid automata (SDHA), to model systems with clocked and unclocked events. Although clocked events can be modeled in standard hybrid automata by introducing additional continuous state variables, we show in this paper how the SDHA formalism provides a basis for more efficient computational methods for verification. Towards this end, we define a transition system semantics for the SDHA and present a method for computing approximate quotient transition systems using a modification of existing tools for computing reachable sets for hybrid systems. The definitions and the elements of a model checking procedure for SDHA are illustrated with an example.