[Back]

S. Gabmeyer, P. Kaufmann, M. Seidl:
"A Feature-Based Classification of Formal Verification Techniques for Software Models";
Report No. BIG-TR-2014-1, 2014; 43 pages.

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 suggests to automatically generate the executable code from these models. Thus, defects in the models most likely propagate to the executable code. To detect defects already at the modeling level many approaches propose to use formal verification techniques to ensure the correctness of 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.

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 suggests to automatically generate the executable code from these models. Thus, defects in the models most likely propagate to the executable code. To detect defects already at the modeling level many approaches propose to use formal verification techniques to ensure the correctness of 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.

Feature-based classification, formal verification techniques, model-based engineering, model checking, theorem proving

http://publik.tuwien.ac.at/files/PubDat_228585.pdf

Project Head Martina Seidl:
FAME: Formalisierung und Handhabung von Evolution in modellbasierter Softwareentwicklung