MVV 2015 - IEEE International Workshop on Model-Based Verification & Validation

Costs entailed by software failures demonstrate that the systematic development of software of a certain
quality is still a challenge, even after decades of research. A reason for this can certainly be found within
the individual projects. Often, known techniques of quality assurance are neither well understood nor
properly used due to deadline and budget restrictions. However, another reason is the lack of techniques
for quality assurance for specific types of software as well as for software developed according to specific
programming and modeling techniques.
Many ad-hoc security specifications, models, and protocols, which were implemented in software
components in the past, turned out to be vulnerable to some extent. Formal verification and validation
methodologies have the potential to increase user confidence in software artifacts. Therefore, theoretical
foundations for security assurance should be investigated to discover new methods that will bring high
certainty to the trustworthiness of software entities.
Verification and validation (V&V) methods, especially testing, deliver important analytical techniques for
quality assurance. In model-based V&V, the software under consideration is represented by means of a
model that focuses on certain aspects, often on the behavior of the software. Finite state machines and
flow graphs are frequently used models. Testing techniques based on such models include, for instance,
formal verification, control and data flow analysis, test case generation, and model checking.