Title :
Automatic verifying approach for product specification using FTA
Author :
Fukaya, T. ; Hirayama, M. ; Mihara, Y.
Author_Institution :
Res. & Dev. Center, Toshiba Corp., Kawasaki, Japan
Abstract :
We propose a verification method for software specification. In order to avoid software faults, our method derives safety assertions using FTA, computes the behavioral graph of specification and analyzes statically whether this graph satisfies safety assertions. Moreover, when there exists an assertion which can not hold, our method localizes software design faults.<>
Keywords :
fault tolerant computing; formal specification; formal verification; software reliability; FTA; automatic verifying approach; behavioral graph; product specification; safety assertions; software faults; software specification; Formal verification; Hardware; Humans; Product safety; Software design; Software engineering; Software quality; Software safety; Temperature control; US Department of Transportation;
Conference_Titel :
Fault-Tolerant Computing, 1994. FTCS-24. Digest of Papers., Twenty-Fourth International Symposium on
Conference_Location :
Austin, TX, USA
Print_ISBN :
0-8186-5520-8
DOI :
10.1109/FTCS.1994.315649
