Data Abstraction without Control Abstraction in Software Model Checking

Опубликовано 6 сентября 2016, 6:30

Data abstraction through predicate abstraction in software model checking requires a theorem proving step to create an abstract version of the program control structure. While this process is effective for programs with simple data manipulations, such as device drivers, abstraction of program control structures can become undecidable and imprecise for more complex, yet reasonable, data manipulations--such as the multiplication of two variables. Data abstractions that do not require the abstraction of program control structures can be applied in the presence of arbitrarily complex data manipulations and support a new method for model checking component- based software. We discuss two such data abstractions. The first is an extension of static dead variable analysis which allows the use of verification- time information to mark more variables dead during verification. In ideal cases, the resulting analysis yields a 75 reduction in the time and space required for model checking. The second application, which is still being developed, is the use of under-approximating predicate abstraction to abstract the component being verified rather than the surrounding software. This approach to software model checking, when combined with an explicit model checker that operates directly on the software artifact (such as the Java PathFinder), may support the verification of more complex components because the surrounding software can be efficiently and deterministically executed while the component is verified in an abstract data domain. In this setting, data abstraction without control abstraction allows the efficient transfer of control between the abstracted component and surrounding software.