AVACS
Automatic Verification and Analysis of Complex Systems
General Information
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 Area R - Real-Time Systems
Real-time systems are systems that interact with their environment in
such a way that for certain inputs the corresponding outputs have to
occur within given time bounds. Many embedded systems, in particular
those in safety critical applications, are of this type. The practical
importance of this class of systems has led to a large body of research
on the specification, verification and analysis of real-time
systems.
Analysis and verification of real-time systems is based on
computational models of such systems. Models with continuous time are
close to the physical world and are well suited for dealing with the
requirement and specification level; their automatic verification is
performed using tools based on timed automata with real-valued
clocks. To gain in efficiency also models with discrete time are
considered; their automatic verification is performed using classical
approaches to temporal logic model checking. At the level of machine
real-time systems are modeled as set of tasks that need to be scheduled
to meet the required deadlines.
While these real-time models have led to powerful analysis and
verifications techniques, they turn out to be too idealistic or too
simplistic to deal with the challenges of high-level specification
languages, highly concurrent systems, and the intricacies of
distributed computer architectures.
The AVACS subprojects R1--3 strive to overcome these restrictions by
exploiting the structure of the real-time systems at all levels of
abstraction ranging from specification level down to implementation
level:
- subproject R1 will develop verification techniques for real-time requirements of high-level specifications based on constraint manipulation, predicate abstraction, and decision procedures for high-level data types;
- subproject R2 will develop task distribution and scheduling techniques taking the constraints of distributed computer architectures into account, in particular the combination of caches and pipelines;
- subproject R3 considers highly concurrent real-time systems and develops model checking techniques that combine heuristic search with abstraction.
Project Area S - Coarse Grain System Structure
Project Area S focuses on techniques to support the global analysis of
the interplay between different systems, or between subsystems, thus
addressing both inter-system and system-level design. Typical instances
in the train system domain relate to the interaction between trains and
track-side elements such as RBC, s, or between the different components
of the on-board electronic subsystems of a train. The overall challenge
for Project Area S is thus the need to address complete systems, or
even systems of systems, demanding dedicated techniques to cater for
the sheer complexity of resulting models. Subproject S1 addresses this
by automating compositional verification; it uses learning strategies
and combinations of abstraction techniques, game theory, and SAT and
model checking based verification methods to automatically synthesize
assumptions, allowing to reduce global verification of (potentially
only partially specified) system level designs to local verification
tasks. The particular challenges of inter-system coordination
protocols, which typically require dynamically changing communication
structures and must address systems entering and leaving surveillance
regions, are attacked in S2 with a combination of static analysis
techniques, abstraction techniques, and symmetry arguments to reduce
the verification of such coordination protocols to finite state
verification problems. Subproject S3 provides formal proofs of system
dependability requirements through stochastic model checking of system
models, taking into account failure models and component failure
behaviors, while deriving safety requirements for subsequent design
steps.
By addressing complete systems and their interplay, Project Area S
provides methods for reducing global verification tasks to smaller
problem instances (S1, S2) and dependability analysis, which inherently
requires global system analysis. Subprojects S1 and S2 complement each
other, in that verification instances resulting from the reduction
methods of S2 can be further decomposed using techniques of S1. Models
used will reflect the particular complexity dimension attacked in each
subproject, providing sufficiently rich structuring methods to
asynchronously compose transition systems, supporting their dynamic
creation and destruction and dynamic communication structures for S2,
and using extended Markov Processes in S3. Later project phases will
enrich the class of models, allowing to deal with real-time and hybrid
component models, and extend decomposition theorems to such richer
classes of models, thus paving the way for realizing the AVACS vision,
where an overall verification methodology invokes such decomposition
theorems, unfolding a proof tree for global problems to a level where
verification tasks can be discharged with the verification methods
developed in Project Areas R and H.
Publications
More Information
If you are interested in more information on AVACS or the different subprojects, please visit www.avacs.org.