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

• 作者: 张兴元 张毓森 杨华兵 王元元 王金双
• 来源期刊: 计算机工程与应用
• 学科: 工学
• 关键词: 电梯控制系统 活动性 形式化验证 Isabelle/HOL/Isar工具
• 年，卷（期）: 2008,（27）
• 所属期刊栏目: 工程与应用
• 页码范围: 216-218
• 页数: 3页
• 分类号: TP301
• 字数: 3420字
• 语种: 中文
• DOI: 10.3778/j.issn.1002-8331.2008.27.069

摘要

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

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	张毓森	解放军理工大学指挥自动化学院	66	580	12.0	22.0
2	王元元	解放军理工大学指挥自动化学院	46	351	12.0	16.0
3	张兴元	解放军理工大学指挥自动化学院	14	20	2.0	3.0
4	王金双	解放军理工大学指挥自动化学院	23	189	4.0	13.0
5	杨华兵	解放军理工大学指挥自动化学院	6	16	3.0	3.0