Formal Modeling and Verification of Systems with Self-x Properties

In this paper we present a case study in formal modeling and verification of systems with self-x properties. The example is a flexible robot production cell reacting to system failures and changing goals. The self-x mechanisms make the system more flexible and robust but endanger its functional correctness or other quality guarantees. We show how to verify such adaptive systems with a ``restore-invariant'' approach.