期刊文献+
任意字段
题名或关键词
题名
关键词
文摘
作者
第一作者
机构
刊名
分类号
参考文献
作者简介
基金资助
栏目信息

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

Liveness reasoning of elevator control system in Isabelle/HOL
下载PDF
导出
摘要 电梯控制系统经常被用于展示形式化验证方法的有效性。将电梯控制系统看作一个并发系统,利用Paulson归纳法对其进行描述。在定理证明工具Isabelle/HOL/Isar中给出了电梯控制系统的活动性证明。该方法能够处理状态空间任意大的电梯控制系统。 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.
作者 王金双 杨华兵 张兴元 王元元 张毓森
机构地区 解放军理工大学指挥自动化学院
出处 《计算机工程与应用》 CSCD 北大核心 2008年第27期216-218,共3页 Computer Engineering and Applications
基金 国家自然科学基金(No.60373068)~~
关键词 电梯控制系统 活动性 形式化验证 Isabelle/HOL/Isar工具 elevator control system liveness formal verification Isabelle/HOL/Isar
分类号 TP301 [自动化与计算机技术—计算机系统结构]
  • 相关文献

参考文献11

  • 1Paulson L C.Mechanizing UNITY in isabelle[J].ACM Trans Comput Logic, 2000,1 ( 1 ) : 3-32.
  • 2Dyck D N,Caines P E.The logical control of an elevator[J].IEEE Trans on Automatic Control, 1995,40(3 ) :480-486.
  • 3Wood W G.Temporal logic case study[C]//LNCS 407:the International Workshop on Automatic Verification Methods for Finite State Systems.Berlin : Springer, 1990 : 257-263.
  • 4Clarke E,Wing J.Formal method:state of the art and future directions CMU-CS-96-178[R].Department of Computer Science,CMU, 1994.
  • 5Paulson L C.The inductive approach to verifying crypographic protocols[J].J Comput Secur, 1998,6(1/2) : 85-128.
  • 6Paulson L C.Verifying the SET protocol:overview[J].ACM Transactions on Computer and System Security,1999,2:332-351.
  • 7Wenzel M.Isabelle/Isar-a generic framework for human-readable proof documents[C]//LNCS 4732:Theorem Proving in Higher Order Logics,TPHOLS 2007, Kaiserslautem, Germany, 2007.
  • 8Nipkow T,Paulson L C,Wenzel M.Isabelle/HOL-a proof assistant for higher-order logic[M].London:Springer-Verlag,2002.
  • 9Zhang X,Yang H,Wang Y.Liveness reasoning for inductive protocol verification[C]//The Emerging Trend of TPHOLs 2005,2005: 221-235.
  • 10Wang J,Zhang X,Zhang Y,et al.A Probabilistic Model for Parameric Fairness in Isabelle/HOL[C]//Theorem Proving in Higher Order Logics: Emerging trends Proceedings, 2007 : 194-209.
计算机工程与应用
2008年 第27期

相关作者

内容加载中请稍等...

相关机构

内容加载中请稍等...

相关主题

内容加载中请稍等...

浏览历史

内容加载中请稍等...
;
使用帮助 返回顶部