The general research idea of SCARE leads to a number of new research questions that we wish to investigate in the RTG. Below we give examples of such questions. For current projects see the section Current and Completed PhD Projects.

Regarding aspect A (limited knowledge), we wish to study the interplay of the parameters Env and Asm and their impact on the satisfaction relation sat in the generic correctness formula (1). This leads for example to the following questions:

• How can we model and maintain the limited knowledge about the dynamics of the environment and its impact on the computerized system?

• How can we achieve and prove safety of a system despite of unsafe information about the environment due to unprecise sensor values?

Regarding aspect B (unpredictable behaviour), we shall interpret the parameter Asm by different assumptions about the model of the (physical) environment and the system, and then investigate suitable variants of the correctness relation sat. More specifically, we consider questions like:

• How can we use quantifiable degradation of components, for instance an increasing latency of aging transistors, in the verification process?

• How can we exploit quantifiable satisfaction relations to obtain more powerful techniques for dealing with fault tolerance, both in the sense of the necessary redundance and the extent of fault masking?

• How can we achieve graceful degradation when the errors occur in system components and/or the environment or when the real system behavior deviates from the model used in the verification process?

Regarding aspect C (changing system environment and system structure), we wish to investigate the robustness of the satisfaction relation sat against changes of the structure of the enviroment Env and the system Sys. This leads for example to the following questions:

• How can we conduct system verification that is robust against changes of resources?

• How to construct models of system dynamics that represent and make analyzable the dependence of the system behavior on the structure the system (e.g., on the number of agents) and its components (e.g., on technical parameters)?

• How can changes of the system realiably be detected and assessed?

Research Themes. In SCARE, the three aspects A, B and C of adverse conditions will considered under the following research themes:

1. Modeling Techniques,

2. Verification and Analysis Techniques,

3. Constructive Techniques, in particular the combination of formal methods with engineering approaches.