Ralf Kneuper: Symbolic Execution as a Tool for Validation of Specifications

PhD Thesis, Dept. of Computer Science, University of Manchester.
Published as Technical Report UMCS-89-7-1

full text (scanned PDF version)

This thesis investigates symbolic execution, a method originally developed for the verification and validation of programs, and extends it to deal with (state-based) specification languages as well.

The main problems encountered are implicit specifications and the intended genericity with respect to the specification language used. Implicit specifications are handled by introducing ‘description values’: identifiers take as values predicates which describe their ‘actual value’, the value one would get by actual execution.

Language genericity is achieved by expressing the definition of symbolic execution in terms of the semantics of the specification language used. Both denotational and operational semantics of symbolic execution are discussed. The denotational semantics of symbolic execution, expressed in terms of the denotational semantics of the specification language, provide a correctness notion for symbolic execution. A description of the operational semantics of the language is used as a parameter to tailor symbolic execution to that language.

Based on these ideas, a symbolic execution system called SymbEx is described and specified. SymbEx is to form part of the project support environment Ipse 2.5 and help the user to validate a specification by symbolically executing it.

Finally, the achievements and limitations of this approach are discussed, and suggestions made for future work.