Use of formal modeling to automatically generate correct fault detection and response methods

摘要

This paper describes an approach to fault tolerant design and implementation that uses a formal model to automatically generate fault detection and response methods. The approach is designed for resource-constrained embedded systems with high reliability requirements such as manned or critical space assets. The formal model-based approach offers several advantages over a conventional approach based on manual failure mode analysis (FMA). The primary benefits are increased confidence in the fault tolerance of the design and in the corresponding implementation. Increased confidence in the design is achieved because both the system architecture and reliability requirements are precisely described in a single formal model written in Answer Set Prolog (ASP). The readability of ASP facilitates precise communication between system engineers and stakeholders, thus increasing the likelihood that design errors are corrected early in the development cycle. Increased confidence in the implementation is achieved because it is automatically generated using the model and is guaranteed to satisfy the specified reliability requirements. Importantly, the control flow of the resulting implementation is straightforward and readable. Besides increased confidence, our approach is resilient to architecture and requirements changes. In our experience, once the model is updated it takes less than 10 minutes to re-generate the implementation and download to the target.