A proof-based method of hybrid systems development using differential invariants
A proof-based method of hybrid systems development using differential invariants
复制标题
使用微分不变量的基于证明的混合系统开发方法
DOI：
10.1007/s11704-018-7213-y
复制
发表时间：
2018-09
影响因子：
4.2
通讯作者：
Mingsong CHEN
中科院分区：
文献类型：
--
作者：
Jie LIU;Jing LIU;Miaomiao ZHANG;Haiying SUN;Xiaohong CHEN;Dehui DU;Mingsong CHEN
Event-B是一种通过改进的广泛应用和基于证明的语言，用于增量开发[1]。混合系统表现出离散控制和实时连续行为的混合特征。但是，Event-B是一种离散的建模语言。它
Event-B is a widely applied and proof-based language for incremental development via refinement [1]. Hybrid systems exhibit hybrid characteristics of discrete control and real-time continuous behaviors. However, Event-B is a discrete modeling language. It does not support the development of hybrid systems. So, the researchers are currently trying to make the extension of Event-B for the refinement development of hybrid systems [2, 3], To minimally change the prototype of Event-B, we used the framework of Event-B as a basis, and studied from four aspects: the modeling method focusing on the continuous behaviors of hybrid systems, proof obligation rules of continuous behavior models, proving techniques, and proving tools.
登录
查看更多内容
DOI：
--
发表时间：
2014
期刊：
Journal of Software
影响因子：
--
作者：
B. Le
通讯作者：
B. Le
DOI：
10.1007/978-3-642-39721-9_5
发表时间：
2013-08
期刊：
--
影响因子：
--
作者：
N. Zhan;Shuling Wang;Hengjun Zhao
通讯作者：
N. Zhan;Shuling Wang;Hengjun Zhao
影响因子：
1.3
作者：
Banach, Richard;Butler, Michael;Zhu, Huibiao
通讯作者：
Zhu, Huibiao
通过计算类李雅普诺夫函数来对一类切换系统的吸引域进行内近似
影响因子：
3.9
作者：
Xiuliang Zheng;Zhikun She;Quanyi Liang;Meilun Li
通讯作者：
Meilun Li
通过计算类 Lyapunov 函数来计算具有目标的不变性核
影响因子：
2.6
作者：
She Zhikun;Xue Bai
通讯作者：
Xue Bai