Early detection of evolving system failures and temporal conflicts using parameterized formal specifications and bounded constraint-solving

摘要

This paper describes an analysis technique for a system consisting of a collection of formal specifications. The goal of the analysis is to provide early discovery of system states from which the system will inevitably fail in the future by violating some formal specification. This goal can also be formulated as a form of temporal specification conflicts. The technique utilizes SAT-solver based bounded constraint solving within a custom search algorithm. The proposed technique is also compared to an alternative model checking of Computational Tree Logic technique. The proposed technique can assist in providing an early warning for a mission critical system such as the power grid prior to an emerging catastrophic failure.