Direct Model Checking Matrix Algorithm
Direct Model Checking Matrix Algorithm作者机构：Department of Computer Science and Technology Peking University Beijing 100871 P.R. China Department of Computer Science Paderborn University D-33095 Germany
出 版 物：《Journal of Computer Science & Technology》 (计算机科学技术学报（英文版）)
年 卷 期：2006年第21卷第6期
页 面：944-949页
核心收录：
学科分类：0808[工学-电气工程] 08[工学] 0835[工学-软件工程] 0701[理学-数学] 0811[工学-控制科学与工程] 0812[工学-计算机科学与技术（可授工学、理学学位）]
主 题：direct model checking (DMC) Kripke semantics structure CTL logic matrix algorithm
摘 要：During the last decade, Model Checking has proven its efficacy and power in circuit design, network protocol analysis and bug hunting. Recent research on automatic verification has shown that no single model-checking technique has the edge over all others in all application areas. So, it is very difficult to determine which technique is the most suitable for a given model. It is thus sensible to apply different techniques to the same model. However, this is a very tedious and time-consuming task, for each algorithm uses its own description language. Applying Model Checking in software design and verification has been proved very difficult. Software architectures （SA） are engineering artifacts that provide high-level and abstract descriptions of complex software systems. In this paper a Direct Model Checking （DMC） method based on Kripke Structure and Matrix Algorithm is provided. Combined and integrated with domain specific software architecture description languages （ADLs）, DMC can be used for computing consistency and other critical properties.
维普期刊数据库