Uni-Logo
Deutsch      
Computer Architecture - Team Bernd Becker
        Startseite         |         Institut für Informatik         |         Technische Fakultät
 

AVACS: Automatic Verification and Analysis of Complex Systems

| project staff | cooperation partners | project description | project target | project structure | Talks |


project staff

former employee Chair of Computer Architecture
Marc Herbstritt, Dr. research assistant
Natalia Kalinnik, Dipl.-Inf. (Working in H1/2.) research assistant
Ilia Polian, Dr. (Working in R2 and H2) research assistant
Erika Ábrahám, Dr. (Working in H2) research assistant
Frank Schmiedle, Dr.-Ing. (Working in S3) research assistant
Jochen Eisinger, Dr. (Working in R2 and H1) research assistant
Chair of Computer Architecture
Angelika Fabry-Flashar (Administration) Administration
Bernd Becker, Prof. Dr. (Co-speaker, Site-Coordinator Freiburg. Working in H1/2, S1, and S3.) Contact
Tobias Schubert, Dr. (Working in H1/2) research assistant
Matthew Lewis, M.Sc.(Eng) (Working in S1) research assistant
Ralf Wimmer, Dipl.-Inf. (Working in H2 and S3) research assistant
Stefan Kupferschmid, Dipl.-Inf. (Working in H1/2) research assistant
Bettina Braitling, Dipl.-Inf. research assistant
Karsten Scheibler, Dipl.-Inf. research assistant
Christian Miller, Dipl.-Inf. research assistant
Peter Winterer, Dipl.-Ing. (FH) (Technical Administration) Technical Administration
cooperation partners

University Of Freiburg
Dagmar Sonntag (Administration) Administration


project description

In the SFB, IRA will conduct joint research with Freiburg's AI, software engineering and operating systems groups, as well as scientists from the universities of Oldenburg, Saarbrücken, the Academy of Sciences of the Czech Republic in Prague and the Max-Planck-Institut Saarbrücken. The project's topic is analysis and formal verification of complex systems. The new European Train Control Standard will be the case study for the evaluation of the developed methods. The contribution of IRA's scientists to the project will be particularly in the area of base technologies. The approval is valid for eight years and can be extended for up to four more years. Young scientists, in particular, will have an excellent opportunity to get strategic competence on verification of hybrid and real-time systems. The approval is also an expression of confidence in our skills by the German Research Council, and we consider it to be an appreciation of the quality of our recent research.

Further informations are available from the [AVACS website]



project target

This project addresses the rigorous mathematical analysis of models of complex safety critical computerized systems, such as aircrafts, trains, cars, or other artifacts, whose failure can endanger human life. Our aim is to raise the state of the art in automatic verification and analysis techniques (v&a) from its current level, where it is applicable only to isolated facets (concurrency, time, continuous control, stability, dependability, mobility, data structures, hardware constraints, modularity, levels of refinement), to a level allowing a comprehensive and holistic verification of such systems.

* We will investigate the mathematical models and their interrelationship as they arise at the various levels of design of safety critical computerized systems. These models range from classical non-deterministic transition systems to probabilistic, real-time, and hybrid system models.
* We will, in particular, deal with the complete range of time-models needed to support the development of concrete systems, and the transition between them. This includes the determination of safe sampling rates in plant control as well as the transition between virtual time models and physical execution time.
* We will also address a wide range of system structures in this application domain. These range from models of distributed target architectures (such as hierarchical bus-structures connecting multiple electronic control units) to task models (depicting hierarchical task structures with communication and timing requirements) to specification models of electronic control units (such as a controller enforcing a speed-profile) to system models (e.g. of the electronic on-board train systems) to inter-system specification models (e.g. for coordination of train movements).

Today's v&a technology at best addresses isolated points in this space of models. The proposed project sets out to develop automatic verification techniques covering the entire space. It is our firm belief that by improving and better automating base verification methods (such as abstract interpretation, SAT solvers, symbolic model checking, abstraction techniques, linear programming, constraint solving, Lyapunov functions, automatic decision procedures for relevant first-order theories, automata based verification, heuristic search) and by integrating them in a deep and focused manner we will be able to achieve a dramatic increase in the complexity of models amenable to automatic verification. (By complexity we mean both system size as well as logical complexity as induced by the interferences between the various facets of the system.) By identifying new, as well as by exploiting well-established design and modeling paradigms (mathematically reflected by decomposition theorems that break down complex systems into manageable sub-systems and facets), the combination of the individual, complementing automated verification techniques will deliver synergies that we do not see in present verification systems.



project structure

The AVACS Colloborative Research Center consists of three areas:

Project area R: Real-time systems
Project area H: Hybrid systems
Project area S: Coarse Grain System Structure

The individual project areas themselves are again divided into several
subprojects:

Project area R:
Subproject R1: Beyond Timed Automata
Subproject R2: Timing Analysis, Scheduling and Distribution of Real-Time Tasks
Subproject R3: Heuristic Search and Abstract Model Checking

Project area H:
Subproject H1/2: Constraint-based Verification for Hybrid Systems
Subproject H3: Automatic Abstraction of Hybrid Controllers
Subproject H4: Automatic Verification of Hybrid System Stability

Project area S:
Subproject S1: Compositional Approaches to System Verification
Subproject S2: Dynamic Communication Systems
Subproject S3: Formal Verification of Availability Properties

Additionally there is a project area Z (Central Services).

More detailed informations on the project structure are available from the [AVACS Website].



Talks

You will find information for viewing the recordings following the link
[Information]


List of Talks