Self-stabilizing Java: Tool Support for Building Robust Software.

摘要

Developing robust software systems remains an open research problem. The current approaches for improving software reliability mainly focus on minimizing the number of software bugs through formal verification or extensive testing. Despite such efforts, it is common that unexpected software bugs corrupt a program's state and cause systems to fail.;The motivation for this research is to embrace the fact that it is difficult to guarantee that software is error-free. We present Self-stabilizing Java (SJava) that instead checks that a program self-stabilizes. Self-stabilizing programs automatically recover to the correct state from the corrupted state caused by software bugs and other sources. A number of applications are inherently self-stabilizing---such programs typically overwrite all non-constant data with new input data.;We have developed a type system and static analyses that together check whether program executions eventually transition from incorrect states to the correct state. We combine this with a code-generation strategy that ensures that a program continues executing long enough to self-stabilize. Furthermore, in order to lower the burden of type annotations, we present an annotation inference algorithm that automatically derives an initial set of annotations. Our experience using SJava indicates that our system successfully checked that several benchmarks were self-stabilizing and effectively inferred annotations for our benchmarks.