<div class="csl-bib-body">
<div class="csl-entry">Gabmeyer, S. (2015). <i>New model checking techniques for software systems modeled with graphs and graph transformations</i> [Dissertation, Technische Universität Wien]. reposiTUm. https://doi.org/10.34726/hss.2015.31361</div>
</div>
-
dc.identifier.uri
https://doi.org/10.34726/hss.2015.31361
-
dc.identifier.uri
http://hdl.handle.net/20.500.12708/4908
-
dc.description
Abweichender Titel laut Übersetzung der Verfasserin/des Verfassers
-
dc.description
Zsfassung in dt. Sprache
-
dc.description.abstract
In today's software, no matter how security and safety critical it may be, defects and failures are common. With the rising complexity of software and our growing dependency on its correct functioning as it permeates our every day life the software development process requires new approaches to integrate formal verification techniques. This thesis presents approaches on efficiently verifying software systems described by model-driven software development artifacts. These artifacts comprise the implementation of the system and consist of both structural and behavioral models. We present two model checking approaches, MocOCL and Gryphon, to verify the temporal specification of a system against its model-based implementation. Central to our approach is the twofold use of graphs to describe the system under verification. First, we describe the admissible static structure of an instance of the system by means of attributed type graphs with inheritance and containment relations, often referred to as metamodel. Second, we represent a state of the system as an object graph that enumerates a system's active objects, the references among them, and their attribute values. A change in the system, e.g., the deletion of an object or the modification of an attribute value, triggers a state change. The behavior of the system is thus described by actions that modify the state of the system. In this thesis we employ graph transformations to model such state-changing actions as they provide suitable means to formally describe modifications on graphs. The specification of the system, on the other hand, is written in our temporal extension of the Object Constraint Language (OCL) that is based on Computation Tree Logic (CTL). A specification written in our CTL extension for OCL, called cOCL, can be verified against a model-based implementation of the system with our explicit-state model checker MocOCL. Gryphon aims to increase the efficiency and scalability of the verification process and implements a symbolic model checking approach, that focuses the verification on safety specifications. The work presented in this thesis also encompasses a survey and a feature-based classification of verification approaches that can be used to verify artifacts of model-driven software development. Methodologically, it provides the motivation for our work on MocOCL and Gryphon. Both our approaches are novel in their own respect; MocOCL for its capability to verify CTL-extended OCL expressions and Gryphon for its use of relational logic to build a symbolic representation of the system that can be verified with any model checker participating in the Hardware Model Checking Competition. Finally, MocOCL and Gryphon are evaluated performance-wise on a set of three representative benchmarks that demonstrate the model checkers' preferred fields of application and its limitations.
en
dc.language
English
-
dc.language.iso
en
-
dc.rights.uri
http://rightsstatements.org/vocab/InC/1.0/
-
dc.subject
Model Checking
de
dc.subject
Model Driven Software Development
de
dc.subject
Model Checking
en
dc.subject
Model Driven Software Development
en
dc.title
New model checking techniques for software systems modeled with graphs and graph transformations
en
dc.title.alternative
New Model Checking Techniques for Software Systems Modeled with Graphs and Graph Transformations
de
dc.type
Thesis
en
dc.type
Hochschulschrift
de
dc.rights.license
In Copyright
en
dc.rights.license
Urheberrechtsschutz
de
dc.identifier.doi
10.34726/hss.2015.31361
-
dc.contributor.affiliation
TU Wien, Österreich
-
dc.rights.holder
Sebastian Gabmeyer
-
tuw.version
vor
-
tuw.thesisinformation
Technische Universität Wien
-
dc.contributor.assistant
Seidl, Martina
-
tuw.publication.orgunit
E188 - Institut für Softwaretechnik und Interaktive Systeme
-
dc.type.qualificationlevel
Doctoral
-
dc.identifier.libraryid
AC12630737
-
dc.description.numberOfPages
145
-
dc.identifier.urn
urn:nbn:at:at-ubtuw:1-87286
-
dc.thesistype
Dissertation
de
dc.thesistype
Dissertation
en
dc.rights.identifier
In Copyright
en
dc.rights.identifier
Urheberrechtsschutz
de
tuw.advisor.staffStatus
staff
-
tuw.assistant.staffStatus
staff
-
tuw.advisor.orcid
0000-0002-4758-9436
-
item.fulltext
with Fulltext
-
item.cerifentitytype
Publications
-
item.mimetype
application/pdf
-
item.openairecristype
http://purl.org/coar/resource_type/c_db06
-
item.languageiso639-1
en
-
item.openaccessfulltext
Open Access
-
item.openairetype
doctoral thesis
-
item.grantfulltext
open
-
crisitem.author.dept
E188 - Institut für Softwaretechnik und Interaktive Systeme