A Formal Specification of Fault Trees for SAM

概要

論文の詳細を見る
With the progress of research on formal methods, formal specifications can now be employed as an effective technique for system development by professionals and practitioners in both academia and industry. In the ASAM project (A Safety Argument Manager), we used Z to specify fault trees, their consistency properties, and various operations for a support system. Through our experience, we find that (1) writing a formal specification is very effective in helping the specifiers identify problems, eliminate the ambiguity, and discover the real requirements for a desired software system from the users; (2) a formal specification may be precise in expression, but may be imprecise for understanding; (3) formal specifications are difficult for engineers to understand so that the role of a formal specification for deriving an implementation is very limited.
一般社団法人情報処理学会の論文
1997-10-15