| 电梯控制系统在Isabelle/HOL中的活动性证明 |
| |
| 引用本文： | 王金双,杨华兵,张兴元,王元元,张毓森.电梯控制系统在Isabelle/HOL中的活动性证明[J].计算机工程与应用,2008,44(27):216-218. |
| |
| 作者姓名： | 王金双 杨华兵 张兴元 王元元 张毓森 |
| |
| 作者单位： | 解放军理工大学 指挥自动化学院，南京 210007 |
| |
| 摘 要： | 电梯控制系统经常被用于展示形式化验证方法的有效性。将电梯控制系统看作一个并发系统，利用Paulson归纳法对其进行描述。在定理证明工具Isabelle/HOL/Isar中给出了电梯控制系统的活动性证明。该方法能够处理状态空间任意大的电梯控制系统。
|
| 关 键 词： | 电梯控制系统 活动性 形式化验证 Isabelle/HOL/Isar工具 |
| 收稿时间： | 2007-11-13 |
| 修稿时间： | 2007-12-28
|
Liveness reasoning of elevator control system in Isabelle/HOL |
| |
| WANG Jin-shuang,YANG Hua-bing,ZHANG Xing-yuan,WANG Yuan-yuan,ZHANG Yu-sen.Liveness reasoning of elevator control system in Isabelle/HOL[J].Computer Engineering and Applications,2008,44(27):216-218. |
| |
| Authors: | WANG Jin-shuang YANG Hua-bing ZHANG Xing-yuan WANG Yuan-yuan ZHANG Yu-sen |
| |
| Affiliation: | College of Command Automation，PLA University of Science and Technology，Nanjing 210007，China |
| |
| Abstract: | Elevator control systems are often used as benchmark problems in formal verifications.The elevator control system is taken as a concurrent system,which is described using Paulson's inductive approach.A liveness proof of the elevator control system is shown in Isabelle/HOL/Isar,which can deal with arbitrary large state space systems. |
| |
| Keywords: | elevator control system liveness formal verification Isabelle/HOL/Isar |
| 本文献已被 CNKI 万方数据 等数据库收录！ |
| 点击此处可从《计算机工程与应用》浏览原始摘要信息 |
|
点击此处可从《计算机工程与应用》下载全文 |
