Efficient software product-line model checking using induction and a SAT solver |
| |
Authors: | Fei He Yuan Gao Liangze Yin |
| |
Affiliation: | 1. Tsinghua National Laboratory for Information Science and Technology (TNList), Tsinghua University, Beijing 100084, China2. Key Laboratory for Information System Security, Ministry of Education, Beijing 100084, China3. School of Software, Tsinghua University, Beijing 100084, China4. Department of Computer Science and Technology, National University of Defense Technology, Changsha 410073, China |
| |
Abstract: | Software product line (SPL) engineering is increasingly being adopted in safety-critical systems. It is highly desirable to rigorously show that these systems are designed correctly. However, formal analysis for SPLs is more difficult than for single systems because an SPL may contain a large number of individual systems. In this paper, we propose an efficient model-checking technique for SPLs using induction and a SAT (Boolean satisfiability problem) solver. We show how an induction-based verification method can be adapted to the SPLs, with the help of a SAT solver. To combat the state space explosion problem, a novel technique that exploits the distinguishing characteristics of SPLs, called feature cube enlargement, is proposed to reduce the verification efforts. The incremental SAT mechanism is applied to further improve the efficiency. The correctness of our technique is proved. Experimental results show dramatic improvement of our technique over the existing binary decision diagram (BDD)-based techniques. |
| |
Keywords: | software product line model checking satisfiability |
本文献已被 SpringerLink 等数据库收录! |
| 点击此处可从《Frontiers of Computer Science》浏览原始摘要信息 |
|
点击此处可从《Frontiers of Computer Science》下载全文 |
|