电梯控制系统在Isabelle/HOL中的活动性证明
王金双,杨华兵,张兴元,王元元,张毓森
Liveness reasoning of elevator control system in Isabelle/HOL
WANG Jin-shuang,YANG Hua-bing,ZHANG Xing-yuan,WANG Yuan-yuan,ZHANG Yu-sen
计算机工程与应用 . 2008, (27): 216 -218 .  DOI: 10.3778/j.issn.1002-8331.2008.27.069