计算机工程与应用
計算機工程與應用
계산궤공정여응용
COMPUTER ENGINEERING AND APPLICATIONS
2008年
27期
216-218
,共3页
王金双%杨华兵%张兴元%王元元%张毓森
王金雙%楊華兵%張興元%王元元%張毓森
왕금쌍%양화병%장흥원%왕원원%장육삼
电梯控制系统%活动性%形式化验证%Isabelle/HOL/Isar工具
電梯控製繫統%活動性%形式化驗證%Isabelle/HOL/Isar工具
전제공제계통%활동성%형식화험증%Isabelle/HOL/Isar공구
电梯控制系统经常被用于展示形式化验证方法的有效性.将电梯控制系统看作一个并发系统,利用Paulson归纳法对其进行描述.在定理证明工具Isabelle/HOL/Isar中给出了电梯控制系统的活动性证明.该方法能够处理状态空间任意大的电梯控制系统.
電梯控製繫統經常被用于展示形式化驗證方法的有效性.將電梯控製繫統看作一箇併髮繫統,利用Paulson歸納法對其進行描述.在定理證明工具Isabelle/HOL/Isar中給齣瞭電梯控製繫統的活動性證明.該方法能夠處理狀態空間任意大的電梯控製繫統.
전제공제계통경상피용우전시형식화험증방법적유효성.장전제공제계통간작일개병발계통,이용Paulson귀납법대기진행묘술.재정리증명공구Isabelle/HOL/Isar중급출료전제공제계통적활동성증명.해방법능구처리상태공간임의대적전제공제계통.
