Language: English  |  中文 

广西民族大学机构知识库 > → 广西民族大学 > → 信息科学与工程学院 > → 期刊论文 >

Please use this identifier to cite or link to this item: http://ir.calis.edu.cn/hdl/530500/4655

Title: On Invariance of Dynamic CTL Model Checking in Iterative Design of Moore Machine-based System
Other Titles: Moore机表示的系统迭代设计动态CTL模型检验的不变性研究
Authors: School of Optoelectronic Information, University of Electronic Science and Technology of China Chengdu 610054
Chengdu Institute of Computer Applications, Chinese Academy of Sciences Chengdu 610041
LI Shao-rong
YANG Shi-han
WU Jin-zhao
Keywords: omputation tree logic
ynamic model checking
iterative design
Moore machine
Issue Date: 2009-07
Publisher: 电子科技大学学报
Citation: 电子科技大学学报,2009, 38(5):669-677
Abstract: Model checking is a promising approach to verifying safety properties of trusted computing systems in the design phase of system-level. Dynamic model checking is the model checking in which the model changes frequently along the design process. A serious problem for dynamic model checking is that the cost of re-checking is too expensive due to model being changed trivially, so a key issue of the problem is to seek invariance in order to avoid the checking repeatedly. An invariance is a true predicate that will remain true throughout a sequence of model checking. In this paper, a formal framework of dynamic model checking is constructed, and an invariance theory is proposed based on an iterative design process of flow control oriented systems described by Moore machines. It is proved that some non-trivial computation tree logic (CTL) properties can be preserved in the iteration
URI: http://ir.calis.edu.cn/hdl/530500/4655
Appears in Collections:期刊论文

Files in This Item:

File Description SizeFormat
Moore机表示的系统迭代设计动态CTL模型检验的不变性研究_英文_.pdf1.24 MBAdobe PDFView/Open
Recommend this item     Add this item as favorite
View Statistics

License: See CALIS IR operational policies.

Number of Online Users: 150     Total of Site Visit: 3769953