My main research topic is software engineering and formal methods in software engineering.
It includes developing of theories and tools in order to achieve high quality software.
Those developments refer to all phases in software development,
i.e., requirements, design, coding, testing, verification, and software evolution.
The research uses formal methods
RESEARCH OUTLINE:
-
Tools for high quality software.
For example, using AspectJ to instrument Design by Contact for Java programs;
automatically create JUnit tests from legacy code; and enforce design decisions in software implementation;
refactoring programs that use contracts; tools that help to design `good' modularity based on Alloy specifications;
improving design decomposition.
-
Testing and Debugging.
For example, Automatically create JUnit tests from legacy code;
locating regression tests; data refinement based testing: generating test cases and test oracle for
Java programs using Alloy specification; refinement-based testing of delta-oriented product lines;
using Bayesian Belief Networks (BBN) for software debugging;
verification-based test case generation for information-flow properties.
-
Verification.
For example, using the same JML specification of linked data structures
for both formal verification (using KeY) and runtime checking (e.g., with the JET tool);
verification of relational Alloy specifications with KeY;
translating Alloy specifications to JML, such that both can be used
together to specify Java classes to be verified with KeY;
constructing sound abstractions of a given program and its (partial) specification, to enable verification with
less auxiliary annotations and prove efforts; slicing for improving software verification (for both KeY and
Dafny verifications); using theorem prover to avoid false positive notification of information flows;
using Dafny to verify nonfunctional requirements, e.g., complexity;
integration of static and dynamic analysis techniques for checking noninterference.
- Reactive systems.
For example, reusing Verilog Designs in Esterel; purification Esterel programs so that they can be verified
using the XEVE tool; transferring statecharts to Esterel and to nuSMV for verification.
-
Other research activities.
template-based code generation; template-Based development on mobile platform;
approaches to reason about early exploration of system decomposition alternatives;
refinement of UML diagrams and adding semantics to UML diagrams;
developing software on mobile devices;
semantics-preserving code-motion refactoring transformations;identifying microservices using functional decomposition.
