A feature-based classification of formal verification techniques for software models

Software models are the core development artifact in model-based engineering ( MBE ). The MBE paradigm promotes the use of software models to describe structure and behavior of the system under development and proposes the automatic generation of executable code from the models. Thus, defects in the models most likely propagate to executable code. To detect defects already at the modeling level, many approaches propose to use formal verification techniques to ensure the correctness of these models. These approaches are the subject of this survey. We review the state of the art of formal verification techniques for software models and provide a feature-based classification that allows us to categorize and compare the different approaches.