Integrating formal specification and verification methods in software development

Abstract

This dissertation is a part of an intended long-term research project with the objectives to make software development more scientific and rigorous, thereby to achieve better software quality and to facilitate automated software production; and has two major components: the design of the specification transition paradigm for software development and the theoretical study of the system specification phase in the paradigm.

First, after an extensive analysis and comparison of various formalisms, a paradigm for integrating various formal specification and verification methods (predicate transition Petri nets, first order temporal logic, the algebraic, the axiomatic, the denotational, and the operational approaches) in software development has been developed. The model more effectively incorporates foremost formalisms than any other models (the Automatic Programming Project [Bal85], the CIP Project [ClP85], the Larch Project [GHW85] and the RAISE Project [MG87]) and has the following distinctive features: (1) specifications are viewed both as a set of products and a set of well-defined steps of a process, (2) specifications (as a set of products) at different development steps are to be written and verified by different formalisms, (3) specification (as a process) spans from the requirement phase to the detailed design phase, (4) specification for both concurrent and sequential software is supported, and (5) specifications for different aspects (concurrent control abstraction, data abstraction, and procedural abstraction) of a piece of software are dealt with separately. Second, an intensive and in-depth investigation of the system specification phase in the paradigm results in:

- a design methodology for predicate transition nets, which incorporates the separate definition technique in Ada [Ada83] and state decomposition technique in Statechart [Har88] into the traditional transformation techniques for Petri nets, and therefore will significantly reduce the design complexity and enhance the comprehensibility of large predicate transition net specifications;

- the establishment of a fundamental relationship between predicate transition nets and first order temporal logic and the design of an algorithm for systematically translating predicate transition nets into equivalent temporal logic formulae. Therefore the goal to combine the strengths of both formalisms, i.e. to use predicate transition nets as a specification method and to use temporal logic as a verification method, is achieved; and

- the discovery of a special temporal logic proof technique based on a Hilbert-style logic system to verify various properties of predicate transition nets and the associated theorems. Thus temporal logic is effectively used as an analysis method for both safety and liveness properties of predicate transition nets.