基于控制周期特征式的线性混合自动机验证

Verification of Linear Hybrid Automata by Periodical Properties on Control States

提出了一种基于归纳法思想的验证方法 ,通过控制周期上特性的描述 ,发现了基于控制周期特征式的线性混合自动机验证方法。这一方法采用定理证明过程来得出归纳证明的结构 ;采用模型检查方法来得出归纳证明的奠基和迭代步。这一方法同时兼顾了模型检查和定理证明的特点 ,用此定理证明更高的自动化程度解决了单用模型检查不能解决的问题 ,得出了对著名案例 GasBurner问题中的参数 3non- leakking≥ 76的最优范围。

This paper proposes an induction based verification method using properties on control states. The verification itself is done with theorem proving while the induction basis and the induction step are verified using model checking. Using this hybrid method, it is possible to verify problems which cannot be verified only with a model checking process. By analyzing the Gas Burner problem with this method, the parameter limit is improved to 3non -leaking≥76.