[Zurück]


Wissenschaftliche Berichte:

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



Kurzfassung deutsch:
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.

Kurzfassung englisch:
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.

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


Elektronische Version der Publikation:
http://publik.tuwien.ac.at/files/PubDat_228585.pdf



Zugeordnete Projekte:
Projektleitung Martina Seidl:
FAME: Formalisierung und Handhabung von Evolution in modellbasierter Softwareentwicklung


Erstellt aus der Publikationsdatenbank der Technischen Universitšt Wien.