| 题名: | bounded model checking of actl formulae |
| 作者: | Chen Wei
; Zhang Wenhui
|
| 会议文集: | Proceedings - 2009 3rd IEEE International Symposium on Theoretical Aspects of Software Engineering, TASE 2009
|
| 会议名称: | 3rd International Symposium on Theoretical Aspects of Software Engineering
|
| 会议日期: | JUL 29-31,
|
| 出版日期: | 2009
|
| 会议地点: | Tianjin, PEOPLES R CHINA
|
| 关键词: | bounded model checking encoding method
; bounded model verification
; computation tree logic
; error-hunting
; encoding
; formal logic
; formal verification
; program debugging
; tree data structures
|
| 出版者: | THIRD INTERNATIONAL SYMPOSIUM ON THEORETICAL ASPECTS OF SOFTWARE ENGINEERING, PROCEEDINGS
|
| 出版地: | 10662 LOS VAQUEROS CIRCLE, PO BOX 3014, LOS ALAMITOS, CA 90720-1264 USA
|
| ISBN: | 978-0-7695-3757-3
|
| 部门归属: | Chen, Wei; Zhang, Wenhui Chinese Acad Sci, Inst Software, Beijing, Peoples R China.
|
| 主办者: | IEEE Comp Soc, IFIP, Tianjin Normal Univ
|
| 英文摘要: | In this paper we give a new and improved Bounded Model Checking encoding method for the universal fragment of CTL (ACTL). More specifically, the new encoding method works for verification of ACTL properties, instead Of error-hunting. Combine our verification encoding and bug-hunting encoding proposed before, we get a Bounded Model Checking procedure that works for both valid and invalid A CTL properties. The underlying idea and intuition are summarized in this paper and we implement our tool BMV (Bounded Model Verification) on top of the well-known model checker NuSMV 2, and conduct experiments that show the strength and weakness of ACTL Bounded Model Checking compared to traditional BDD-based model checking procedure. |
| 内容类型: | 会议论文
|
| URI标识: | http://ir.iscas.ac.cn/handle/311060/8306
|
| Appears in Collections: | 计算机科学国家重点实验室 _会议论文
|
|
There are no files associated with this item.
|
| Recommended Citation: | |
Chen Wei,Zhang Wenhui. bounded model checking of actl formulae[C]. 见:3rd International Symposium on Theoretical Aspects of Software Engineering. Tianjin, PEOPLES R CHINA. JUL 29-31,.
|
|
|
