SCARE

System Correctness Under Adverse Conditions

The SCARE project, funded by the German Research Foundation (DFG), is focused on the challenges faced by wireless sensing systems operating in dynamic and potentially unpredictable environments. These systems must maintain desired behavioral properties despite the changing conditions they encounter—a concept referred to as system correctness. SCARE’s research is vital as it tackles the complexities of ensuring system safety and functionality when faced with only partially predictable or adverse conditions that can significantly influence both system behavior and the context in which the system operates.

To delve deeper into these challenges, SCARE has identified specific research questions and themes across three primary aspects:

  • Limited Knowledge (Aspect A): The project explores the interplay between the environment (Env) and the system assumptions (Asm), focusing on their impact on the satisfaction relation (sat) in the correctness formula. Key questions include:
    • How to model and maintain knowledge about the dynamic environment and its impacts on the system?
    • How to ensure and prove system safety despite uncertain or inaccurate information from environmental sensors?
  • Unpredictable Behavior (Aspect B): This aspect involves analyzing different assumptions about the environmental and system models to refine the correctness relation (sat). Research questions in this area include:
    • How can the degradation of components, such as aging transistors which may increase latency, be incorporated into the verification process? What methods can be developed to enhance fault tolerance strategies, including necessary redundancy and fault masking capabilities?
    • How can systems be designed to degrade gracefully when discrepancies arise between the modeled and actual system behaviors or component failures occur?
  • Changing System Environment and Structure (Aspect C): SCARE investigates how the robustness of the satisfaction relation (sat) can be maintained amidst changes in the system's environment (Env) and structure (Sys). Important questions here are:
    • How can verification processes remain robust against resource changes?
    • How to model and analyze system dynamics to reflect the dependency of system behavior on its structure and components?
    • How can changes in the system be reliably detected and assessed?

The research themes in SCARE encompass modeling techniques, verification and analysis techniques, and constructive techniques that combine formal methods with engineering approaches. By addressing these themes, SCARE aims to advance the field of system verification under adverse conditions, thereby enhancing the reliability and safety of complex system interactions in unpredictable environments. This comprehensive approach not only pushes the boundaries of current methodologies but also contributes to the foundational understanding necessary for future technological advancements in wireless sensing systems.