电梯控制系统在Isabelle/HOL中的活动性证明
Liveness reasoning of elevator control system in Isabelle/HOL作者机构：解放军理工大学指挥自动化学院南京210007
出 版 物：《计算机工程与应用》 (Computer Engineering and Applications)
年 卷 期：2008年第44卷第27期
页 面：216-218页
核心收录：
学科分类：08[工学] 081202[工学-计算机软件与理论] 0812[工学-计算机科学与技术（可授工学、理学学位）]
主 题：电梯控制系统 活动性 形式化验证 Isabelle/HOL/Isar工具
摘 要：电梯控制系统经常被用于展示形式化验证方法的有效性。将电梯控制系统看作一个并发系统,利用Paulson归纳法对其进行描述。在定理证明工具Isabelle/HOL/Isar中给出了电梯控制系统的活动性证明。该方法能够处理状态空间任意大的电梯控制系统。
维普期刊数据库
同方期刊数据库