Departmental Bulletin Paper Automatic Transformation from SOFL Formal Specifications to Functional Scenario Forms for Verification and Validation

Yan, Ye

Abstract— Specification-based testing and inspection are two important techniques in the SOFL method for verifying programs, but both of them are established on the basis of the concept known as functional scenario form (FSF). In this paper, we describe how a SOFL formal specification can be automatically transformed into a FSF. The transformation is realized in four steps: lexical analysis of the formal specification, conversion from the specification to Reverse Polish Notation (RPN), transformation from RPN to Disjunctive Normal Form (DNF), and derivation of a FSF from the DNF. Our discussion focuses on the first three steps that have already been realized, but we will also discuss how an existing algorithm can be used for the conversion from the DNF to a FSF for verification and validation. We present the related algorithms and ilustrate them with examples. Finally, we evaluate our algorithms implemented in the tool by testing. Keywords— SOFL specification, Lexical Analyzer, RPN, DNF, FSF, verification and validation

Number of accesses :  

Other information