The RTG SCARE addresses hardware and software systems that are placed in an environment with which they cooperate. In gerneral, both the system and the environment consist of a number of components that again cooperate with each other. System correctness means that the cooperation between environment and system satisfies a given specification of desired behavioural properties. Typically, correctness depends on (possibly implicit) assumptions concerning the environment and the components of the system. Symbolically, we express system correctness by the formula

1. Asm ⊢ (Env ∥ Sys) sat Spec

where the parameters represent the following: Asm the set of assumptions, the symbol ⊢ validity, Env the environment, Sys the system, the symbol ∥ their parallel composition, sat the satisfaction relation, and Spec the specification. So (1) states that under the assumptions Asm, the system Sys working in parallel with the environment Env satisfies (or is correct w.r.t.) the specification Spec.

The generic formula (1) can be instantiated in many ways. For example, in classical Hoare's Logic for the correctness of sequential programs, Sys denotes a programm, Env the set of all input values, Spec a pair consisting of precondition and postcondition, sat expresses total correctness, and Asm the assumption that accesses to array variables observe the bounds of their subcripts. In an application to the safety of traffic agents, Sys could represent our own vehicle, Env the other vehicles and the road, Spec the requirement of collision freedom, and sat the satisfaction of this requirement, where the assumption Asm that the brakes will function properly within certain tolerances. An assumption can thus refer to a parameter of a detailed dynamic model of technical components.

SCARE systematically investigates the problem of system correctness in the sense of (1) under adverse, only partially predictable conditions which can influence the behaviour of the system, the system context, and the assumptions made for verifying correctness. The RTG will consider three aspects of adverse conditions, both individually and in their combination:

1. Limited knowledge. We consider systems that cooperate with a partially unknown environment or that can sense their environment only in an unprecise way.

2. Unpredictable behaviour. We consider systems that exhibit sporadic and persistent errors of different kinds as well as environments that behave unpredictable. The system errors may be caused by design errors, by aging of the equipment, or by environmental effects occuring at runtime.

3. Changing system environment and system structure. We consider systems that move in space and time and thus change their context as well as systems and environments where the structures change over time.

The main aim of SCARE is research into notions of system correctness that guarantee robustness of the system behaviour under such adverse conditions. The parameters of (1) will be adapted according to the expertise of the supervisors and the aims of SCARE. For example, to meet the challenges A, B or C, the satisfaction relation sat will be interpreted in different ways: as a classical binary relation ("holds" or "does not hold"), as metric relation ("holds with a certain deviation"), or as a probabilistic relation ("holds with a certain probability"). Also the other parameters of (1) will be interpreted or adapted according to the needs.