Model Checking Software Requirement Specifications Using Domain Reduction Abstraction

Abstract

Model checking techniques have not been effective in important classes of software systems characterized by large (or infinite) input domains with interrelated linear and non-linear constraints over the input variables. In a previous paper we proposed domain reduction abstraction based on data equivalence and trajectory reduction as an alternative and complement to other abstraction techniques. Domain reduction abstraction applies the abstraction to the input domain (environment) instead of the model. In this paper, we describe a prototype integration of thetechnique in the NuSMV symbolic model checker and illustrate its applicability in the context of model checking software requirements specifications. Results from the verification of three industrial size avionics systems demonstrates the feasibility of the approach.