计算机工程与应用 ›› 2008, Vol. 44 ›› Issue (27): 216-218.DOI: 10.3778/j.issn.1002-8331.2008.27.069

• 工程与应用 • 上一篇    下一篇

电梯控制系统在Isabelle/HOL中的活动性证明

王金双,杨华兵,张兴元,王元元,张毓森   

  1. 解放军理工大学 指挥自动化学院，南京 210007
  • 收稿日期:2007-11-13 修回日期:2007-12-28 出版日期:2008-09-21 发布日期:2008-09-21
  • 通讯作者: 王金双

Liveness reasoning of elevator control system in Isabelle/HOL

WANG Jin-shuang,YANG Hua-bing,ZHANG Xing-yuan,WANG Yuan-yuan,ZHANG Yu-sen   

  1. College of Command Automation，PLA University of Science and Technology，Nanjing 210007，China
  • Received:2007-11-13 Revised:2007-12-28 Online:2008-09-21 Published:2008-09-21
  • Contact: WANG Jin-shuang

PDF

摘要： 电梯控制系统经常被用于展示形式化验证方法的有效性。将电梯控制系统看作一个并发系统，利用Paulson归纳法对其进行描述。在定理证明工具Isabelle/HOL/Isar中给出了电梯控制系统的活动性证明。该方法能够处理状态空间任意大的电梯控制系统。

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.

京ICP备13024262号-1
Copyright © 《计算机工程与应用》编辑部
技术支持：北京玛格泰克科技发展有限公司
总访问量
今日访问
在线人数