Abhishek Dubey, Nagabhushan Mahadevan, Gabor Karsai
2012
Formal models of component interactions are essential for safety-critical systems where correctness cannot be verified through testing alone. This work is significant in providing rigorous specifications that enable automated reasoning about system behavior and support synthesis of fault management strategies tailored to specific failure scenarios.
This technical report presents a formal component model for ARINC-653 real-time systems, defining component execution states (active, passive, inactive) and interaction semantics. The work provides mathematical foundations for reasoning about component assemblies and supports automated synthesis of health management strategies.
The formal model captures component port execution semantics through detailed state machines and constraint specifications. It enables derivation of fault propagation patterns and supports automated generation of monitoring and mitigation strategies from component assembly specifications.
@techreport{Dubey2012c,
author = {Dubey, Abhishek and Mahadevan, Nagabhushan and Karsai, Gabor},
institution = {Insitute for Software Integrated Systems, Vanderbilt University},
title = {The Inertial Measurement Unit Example: A Software Health Management Case Study},
year = {2012},
month = {02/2012},
number = {ISIS-12-101},
abstract = {This report captures in detail a Two-level Software Health Management strategy on a real-life example of an Inertial Measurement Unit subsystem. We describe in detail the design of the component and system level health management strategy. Results are expressed as relevant portions of the detailed logs that shows the successful adaptation of the monitor/ detect/ diagnose/ mitigate approach to Software Health Management.},
attachments = {http://www.isis.vanderbilt.edu/sites/default/files/TechReport_IMU.pdf},
contribution = {lead},
file = {:Dubey2012c-The_Inertial_Measurement_Unit_Example.pdf:PDF},
issn = {ISIS-12-101},
keywords = {component models, formal methods, ARINC-653, real-time systems, fault propagation, health management},
tag = {platform}
}