Ensuring Reliability in Self-Adaptive Systems: A Framework for Formal Specification and Verification

Abstract

Self-adaptive systems are designed to maintain functionality and tolerate faults in dynamic and unpredictable environments by adjusting their behavior during runtime. Ensuring the correctness of these adaptations is crucial, especially in safety-sensitive applications. This paper presents a formal verification methodology to validate such systems’ reliability and adaptive correctness. The approach is demonstrated through a mining robotic arm case study, where system behaviors are formally specified using Duration Calculus. These specifications are then systematically mapped to a PRISM model. Using the PRISM model checker, the design is rigorously verified against both functional and non-functional constraints, which include liveness, safety, and deadlock-freeness. The results indicate that the system maintains correct operation with over 99.9% reliability, even under conditions of uncertainty. This framework enhances the target system’s fault tolerance and broad applicability to other self-adaptive systems operating in dynamic environments.