Reviews of specifications for fault detection can reduce the cost and risk of soft-ware projects because faults can be eliminated in the early phases of their development (e.g., requirements specification, design specification). In order to make reviews on a large scale effective, it is important to use a systematic method that allows the reviewer to focus on a manageable component at each time and provies an automatic analysis based on the reviews of all the related components. In this paper we put forward a rigrous reviews method for the verification of formal specifications based on fault tree analysis. Taking SOFL as the target specification language, we describe principles for constructing fault trees, and an application of the proposed technique to the specification of a Railway Crossing Controller.
展开▼