文献类型：期刊文献

中文题名：基于控制周期特征式的线性混合自动机验证

英文题名：Verification of Linear Hybrid Automata by Periodical Properties on Control States

作者：潘国强[1];虞慧群[1];宋国新[1];邵志清[1]

机构：[1]华东理工大学计算机科学与工程系,上海200237

年份：2000

卷号：26

期号：5

起止页码：471

中文期刊名：华东理工大学学报（自然科学版）

外文期刊名：Journal of East China University of Science and Technology

收录：CSTPCD;;国家哲学社会科学学术期刊数据库;EI(收录号：2001015500643);Scopus;北大核心:【北大核心1996】；CSCD:【CSCD2011_2012】；

基金：国家自然科学基金! ( 6970 30 0 8;6990 30 0 4 );上海市高等学校青年科学基金!( 98Q16);国防科技重点实验室基金!( 99JS94 .10 .1.D

语种：中文

中文关键词：模型检查;定理证明;线性混合自动机

外文关键词：formal methods; model checking; theorem proving; linear hybrid automaton

摘要：提出了一种基于归纳法思想的验证方法 ,通过控制周期上特性的描述 ,发现了基于控制周期特征式的线性混合自动机验证方法。这一方法采用定理证明过程来得出归纳证明的结构 ;采用模型检查方法来得出归纳证明的奠基和迭代步。这一方法同时兼顾了模型检查和定理证明的特点 ,用此定理证明更高的自动化程度解决了单用模型检查不能解决的问题 ,得出了对著名案例 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.