 |
|
Research Group: "Static Analysis of Dynamically Evolving
Systems" (SANDS)
|
|
Members
|
Junior Research Group Leader Barbara König
Research Assistant/PhD student Tobias Heindel
Research Assistant/PhD student Vitali Kozioura
Student Research Assistants: Olha Danylevych, Martin Horsch, Ganna Monakova
|
| Group picture
|  |
|
Funding
| DFG project within the "Aktionsplan Informatik" (Emmy Noether Programme)
|
|
Start
| Spring 2004
|
|
Research
|
Modern software systems must meet increasingly higher safety,
security, and reliability standards. At the same time a new
dimension of complexity is introduced by dynamic features: At
program level, modern code relies on dynamic creation of objects and
dynamic dispatch of methods. At system level, communication
protocols, computer networks, and ubiquitous computing systems
exhibit complex features involving process migration, remote
execution or dynamic reconfiguration.
The aim of the research group "Static Analysis of Dynamically
Evolving Systems" is to develop verification and analysis methods
for such dynamically evolving systems. Our approach focusses on a
foundational specification technique for distributed and mobile
systems, so-called graph transformation systems. In this framework
dynamic features are modelled in a natural way by means of
transformation rules over graphs, which represent system states.
Our automatic analysis techniques are based on established general
methods such as abstract interpretation, type systems and model
checking. In order to come to terms with the inherent difficulties in
the analysis of graph transformation systems, we are also using more
specific concepts such as graph morphisms and specialized techniques,
e.g., unfoldings and approximation by Petri nets.
Finally our research includes the adaptation of different logical
frameworks and specification languages to express properties of
graph transformation systems and in order to use them as input
for our verification tools.
|
|
Publications
|
(since Spring 2004) |
| Tools
| Augur - An unfolding-based verification tool for traph
transformation systems |
|
|
|
as