TU München - Fakultät für Informatik
Software- and Systems Engineering Research Group

  Home  |  Forschung/Kompetenz  |  Lehre  |  Personen  |  Publikationen  |  Abschlussarbeiten  |  Sonstiges  |  Kontakt  | 

Agenda

Es sprechen Studenten über ihre abgeschlossenen Diplomarbeiten und Systementwicklungsprojekte.

Am Mittwoch, 06.11.19, ab 11:00 Uhr, im Raum Alonzo Church (01.09.014):

Model Checking Eclipse/EMF Specifications of Dynamic Architectures

The purpose of software architectures is to provide a blueprint, which specifies properties of software systems. By verifying software architectures, flaws in the design can be revealed. In dynamic architectures the structure of an architecture can change during run time, making its verification challenging. Our approach is to use a combination of model checking and interactive theorem proving to verify dynamic architectures. Thereby, component types are first verified against their contracts with the model checker nuXmv. Then, the composition of contracts is verified with the interactive theorem prover Isabelle/HOL. Our implementation is based on FACTum Studio, a tool that already supports the specification and verification of dynamic architectures with interactive theorem proving. However, FACTum Studio does not yet support the modeling of component behavior and its verification against their contracts. Therefore, we extend the functionality of FACTum Studio with the specification of component behavior in terms of state machines and apply model checking to verify it against their contracts. Furthermore, we demonstrate the functionality of our approach by means of a running example and a case study. Our findings suggest that the approach is feasible to verify dynamic architectures. However, our work could benefit by automating parts of the proof for Isabelle/HOL, thus future work should concentrate in this area.

Modellierung von erweiterten Abhängigkeiten in Ursache-Wirkungs-Modellen

Cause-Effect Graphing is a method for requirements testing, to transform textual specifications into specifications of formal language. These formal specifications can then be used to generate test cases automatically. With the help of constraints, impossible test conditions can be excluded and therefore useless test cases eliminated. The goal for this work was to integrate the functionality of constraints as good as possible into an existing tool for generating CEG-diagrams called Specmate. Furthermore, we wanted to enhance the usability of constraints in diagrams for practice.

Interactive Learning of Cause-Effect-Patterns

Requirements engineering is of vital importance for the success of any software engineering project, as it is the starting point for further phases and the foundation for communication and development. Hence it is of major importance to minimize the number of mistakes committed in this phase: flaws in the requirements engineering phase carry over to other phases and it has been proven that the cost for fixing an error increases substantially the later it is found. Since the requirements defined in this stage are later to be reused as test cases, flawless requirements engineering is vital to ensure a reliable verification of development iterations. Approaches utilizing natural language processing have been implemented to aid the process of identifying requirements in natural language and formalizing them. This provides the opportunity for an automatic test case generation from a requirements document. Textual requirements are often verbalized in the form of causal sentences where the implied causality describes the relation of states and processes, that make up the requirement. Extracting causation from natural language has become a potent field of research in requirements engineering. The challenge of detecting and extracting causalities from textual requirements is that the natural language is composed of an elusive variety of rules. This set of rules is difficult to encompass when attempting to define it manually. The approach of this thesis is to combine natural language processing with a machine learning component in order to substitute the explicit definition of causation patterns for a dynamic, interactive learning algorithm. Genetic algorithms aid in extracting the cause- and effect-expressions from the given sentences. The thesis shows that the learning algorithm provides the opportunity to cope with the complexity of natural language and presents a viable approach on automatizing natural language processing in the field of requirements engineering.