Using formal methods to develop a paradigm for software design.

摘要

Formal methods have been used to analyze the properties of many kinds of systems. Over the past several years, a group at Argonne National Laboratory has been investigating the use of formal analysis techniques to study the behavior of fault tolerance in reactor control systems. This investigation has revealed that the key issue in modeling and qualifying fault tolerance properties is independence. Traditional verification tools (including formal analysis) deal with the issue of independence implicitly. For example, fault-injection testing may discover an instance where independence is not maintained when a system crash results from the injection of a single fault. However, this discovery is an effect of the method, in contrast to being a behavior for which the analysis is explicit. In contrast, the approach we describe here is based on the determination of essential system properties and the development of an analysis strategy that facilitates a formalization of that property within the context of the design. 9 refs.