BDD-based software verification Applications to event-condition-action systems

作     者：Beyer, Dirk Stahlbauer, Andreas 

作者机构：Univ Passau D-94032 Passau Germany 

出 版 物：《INTERNATIONAL JOURNAL ON SOFTWARE TOOLS FOR TECHNOLOGY TRANSFER》 (国际技术传输软件工具杂志)

年 卷 期：2014年第16卷第5期

页      面：507-518页

核心收录：

学科分类：08[工学] 0835[工学-软件工程] 0812[工学-计算机科学与技术（可授工学、理学学位）] 

主　　题：Binary decision diagram BDD Symbolic model checking Software model checking Program analysis Event-condition-action system RERS challenge Configurable software verification CPA 

摘      要：In software model checking, most successful symbolic approaches use predicates as representation of the state space, and SMT solvers for computations on the state space;BDDs are often used as auxiliary data structure. Although BDDs are applied with great success in hardware verification, BDD representations of software state spaces were not yet thoroughly investigated, mainly because not all operations that are needed in software verification are efficiently supported by BDDs. We evaluate the use of a pure BDD representation of integer values, and focus on a particular class of programs: event-condition-action (ECA) programs with limited operations. A symbolic representation using BDDs seems appropriate for ECA programs under certain conditions. We configure a program analysis based on BDDs and experimentally compare it to four approaches to verify reachability properties of ECA programs: an explicit-value analysis, a symbolic bounded-loops analysis, a predicate-abstraction analysis, and a predicate-impact analysis. The results show that BDDs are efficient for a restricted class of programs, which yields the insight that BDDs could be used selectively for variables that are restricted to certain program operations (according to the variable s domain type), even in general software model checking. We show that even a naive portfolio approach, in which after a pre-analysis either a BDD-based analysis or a predicate-impact analysis is performed, outperforms all above-mentioned analyses.