首页|期刊导航|计算机工程与应用|电梯控制系统在Isabelle/HOL中的活动性证明

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

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

计算机工程与应用2008，Vol.44Issue(27)：216-218,3.

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

Liveness reasoning of elevator control system in Isabelle/HOL

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

作者信息

1. 解放军理工大学,指挥自动化学院,南京,210007
折叠

摘要

关键词

电梯控制系统/活动性/形式化验证/Isabelle/HOL/Isar工具

分类

计算机与自动化

引用本文复制引用

王金双,杨华兵,张兴元,王元元,张毓森..电梯控制系统在Isabelle/HOL中的活动性证明[J].计算机工程与应用,2008,44(27):216-218,3.

基金项目

国家自然科学基金(the National Natural Science Foundation of China under Grant No.60373068). （the National Natural Science Foundation of China under Grant No.60373068）

计算机工程与应用

OA北大核心CSCDCSTPCD

ISSN：1002-8331

访问量1

下载量0

段落导航