A rigorous approach to reviewing formal specifications

Author

Liu, Shaoying

Author_Institution

Dept. of Comput. Sci., Hosei Univ., Tokyo, Japan

fYear

2002

fDate

5-6 Dec. 2002

Firstpage

75

Lastpage

81

Abstract

A new approach to rigorously reviewing formal specifications to ensure their internal consistency and validity is forwarded. This approach includes four steps: (1) deriving properties as review targets based on the syntax and semantics of the specification, (2) building a review task tree to present all the necessary review tasks for each property, (3) carrying out reviews based on the review task tree, and (4) analyzing the review results to determine whether faults are detected or not. We apply this technique to the SOFL specification language, which is an integrated formalism of VDM, Petri nets, and data flow diagrams to discuss how each step is performed.

Keywords

Petri nets; Vienna development method; computational linguistics; data flow graphs; formal specification; formal verification; software reviews; specification languages; Petri nets; SOFL specification language; VDM; data flow diagram; formal specification; software reviews; Computer science; Documentation; Fault detection; Formal specifications; Performance analysis; Petri nets; Risk analysis; Software performance; Software testing; Specification languages;

fLanguage

English

Publisher

ieee

Conference_Titel

Software Engineering Workshop, 2002. Proceedings. 27th Annual NASA Goddard/IEEE

Print_ISBN

0-7695-1855-9

Type

conf

DOI

10.1109/SEW.2002.1199452

Filename

1199452