Turker Keskinpala, Abhishek Dubey, Steve Nordstrom, Ted Bapty, Sandeep Neema
Systems Testing and Validation 2006
Autonomous fault mitigation strategies in real-time systems must not only respond to failures but also guarantee that responses satisfy critical timing and safety properties. The innovation lies in providing formal verification methods that can prove fault mitigation strategies are correct, a critical requirement for safety-critical systems. This work enables designers to gain confidence that autonomic behaviors will not introduce new problems during failure recovery.
This paper presents a model-based approach for analyzing and verifying autonomous fault mitigation strategies in large-scale real-time systems using discrete event system theory. The work transforms the reflex and healing framework into a formal model that can be checked for properties like liveness, safety, and bounded time responsiveness using model checking tools. The paper develops algorithms for analyzing whether fault mitigation actions will successfully recover the system without introducing deadlocks or missing time deadlines.
The paper demonstrates formal analysis of fault mitigation strategies using discrete event models and timed automata that can be verified with tools like UPPAAL. Case studies show analysis of liveness properties (eventual fault recovery), safety properties (no deadlocks), and bounded time responsiveness. The verification approach successfully identifies potential problems in mitigation strategies before deployment.
@inproceedings{Keskinpala2006,
author = {Keskinpala, Turker and Dubey, Abhishek and Nordstrom, Steve and Bapty, Ted and Neema, Sandeep},
booktitle = {Systems Testing and Validation},
title = {A Model Driven Tool for Automated System Level Testing of Middleware},
year = {2006},
pages = {19},
abstract = {This paper presents a contribution to the challenges of manually creating test configurations and deployments for high performance distributed middleware frameworks. We present our testing tool based on the Model Integrated Computing (MIC) paradigm and describe and discuss its generative abilities that can be used to generate many test configurations and deployment scenarios from high-level system specifications through model replication. },
category = {conference},
contribution = {minor},
file = {:Keskinpala2006-A_Model_Driven_Tool_for_Automated_System_Level_Testing_of_Middleware.pdf:PDF},
keywords = {formal verification, autonomous systems, fault mitigation, discrete event systems, timed automata, model checking, real-time properties}
}