|
|||||
|
|
| 基于控制周期特征式的线性混合自动化验证 | |
| 引用本文： | 潘国强,虞慧群.基于控制周期特征式的线性混合自动化验证[J].医学教育探索,2000(5):471-476. |
| 作者姓名： | 潘国强 虞慧群 |
| 作者单位： | 华东理工大学计算机科学与工程系,上海 |
| 基金项目： | 中国科学院资助项目，上海市高等学校青年科学基金，国防重点实验室基金，69703008,69903004，98Q16，99JS94.10.1.DZ4201，，， |
| 摘 要： | 提出了一种基于归纳法思想的验证方法，通过控制周期上特性的描述，发现了基于控制周期特征式的线性混合自动机验证方法，这一方法采用定理证明过程来得出归纳证明的结构；采用模型检查方法来得出归纳证明的奠基和迭代步，这一方法同时兼顾了模型检查和定理证明的特点用此定理证明更高的自动化程度解决了单用模型检查不能解决的问题，得出了对著名案例ＧａｓＢｕｒｎｅｒ问题中的参数３ｎｏｎ＿ｌｅａｋｋｉｎｇ≥７６的最优范围。 |
| 关 键 词： | 模型检查 定理证明 线性混合自动机 |
Verification of Linear Hybrid Automata by Periodical Properties on Control States |
|
| PAN Guo-qiang,YU Hui-qun,SONG Guo-xin,SHAO Zhi-qing.Verification of Linear Hybrid Automata by Periodical Properties on Control States[J].Researches in Medical Education,2000(5):471-476. | |
| Authors: | PAN Guo-qiang YU Hui-qun SONG Guo-xin SHAO Zhi-qing |
| Abstract: | |
| Keywords: | formal methods model checking theorem proving linear hybrid automaton |
| 点击此处可从《医学教育探索》浏览原始摘要信息 | |
| 点击此处可从《医学教育探索》下载免费的PDF全文 | |