<div class="csl-bib-body">
<div class="csl-entry">Widl, M. (2016). <i>Symbolic methods for the verification of software models</i> [Dissertation, Technische Universität Wien]. reposiTUm. https://doi.org/10.34726/hss.2016.36020</div>
</div>
-
dc.identifier.uri
https://doi.org/10.34726/hss.2016.36020
-
dc.identifier.uri
http://hdl.handle.net/20.500.12708/6019
-
dc.description
Zusammenfassung in deutscher Sprache
-
dc.description.abstract
One of the major challenges in modern software engineering is dealing with the increasing complexity of software systems. The new paradigm of model-driven engineering (MDE) promises to handle this complexity using the abstraction power of software models based on languages such as the Unified Modeling Language (UML). The objective of MDE is to generate executable code from a set of diagrams with little or no intervention of a developer. These diagrams are referred to as model of the system to be implemented. Usually multi-view models are employed, where each diagram shows a different view on the system, altogether providing a holistic representation. This shift from code-centric development to MDE requires a modeling language based on a solid formal semantics, which is considered one of the major current challenges in MDE research and in future improvements of the UML. Further, with this high valorization of software models, also stronger requirements on their consistency come along since errors introduced on the model level can result in faulty code. The models are central to the evolution of a software system and therefore undergo continuous and often parallel modifications that can introduce inconsistencies. However, necessary consistency management tasks are often too cumbersome to be performed manually due to the size of the models. Hence, automated methods are required. In this work we formalize a modeling language based on the UML. Our language contains two views: the state machine diagram and the sequence diagram. We then identify three problems that can occur in models based on this language. The Sequence Diagram Merging Problem deals with merging two modified versions of a sequence diagram in a way that keeps them consistent with the set of state machines they are related to. The State Machine Reachability Problem asks whether a combination of states in a set of state machines can be reached from some global state by sending and receiving messages between the state machines. The Sequence Diagram Model Checking Problem asks whether a sequence diagram is consistent with the set of state machines it instantiates. For each problem, we propose an encoding to the satisfiability problem of propositional logic (SAT) in order to solve it with an off-the-shelf SAT solver and we determine its computational complexity. We evaluate our approaches based on a set of handcrafted models and on grammar-based whitebox fuzzing, for which we develop a random model generator. The results of our experiments show that we can solve instances of these problems of reasonable size on standard hardware with state-of-the-art SAT solvers.
en
dc.language
English
-
dc.language.iso
en
-
dc.rights.uri
http://rightsstatements.org/vocab/InC/1.0/
-
dc.subject
Software models
en
dc.subject
formal semantics
en
dc.subject
model-driven engineering
en
dc.subject
verification
en
dc.subject
satisfiability
en
dc.title
Symbolic methods for the verification of software models
en
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.2016.36020
-
dc.contributor.affiliation
TU Wien, Österreich
-
dc.rights.holder
Magdalena Widl
-
dc.publisher.place
Wien
-
tuw.version
vor
-
tuw.thesisinformation
Technische Universität Wien
-
dc.contributor.assistant
Seidl, Martina
-
tuw.publication.orgunit
E184 - Institut für Informationssysteme
-
dc.type.qualificationlevel
Doctoral
-
dc.identifier.libraryid
AC13072796
-
dc.description.numberOfPages
128
-
dc.identifier.urn
urn:nbn:at:at-ubtuw:1-1008
-
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
-
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
E193-07 - Forschungsbereich Visual Analytics
-
crisitem.author.parentorg
E193 - Institut für Visual Computing and Human-Centered Technology