The integration of software specification, verification, and testing techniques with software requirements and design processes.

Specifying, verifying, and testing software requirements and design are very important tasks in
the software development process and must be taken seriously. By investing more up-front
effort in these tasks, software projects will gain the benefits of reduced maintenance costs,
higher software reliability, and more user-responsive software. However, many individuals
involved in these tasks still find that the techniques available for the tasks are either too
difficult and far from practical or if not difficult, inadequate for the tasks.
This thesis proposes practical and capable techniques for specifying and verifying
software requirements and design and for generating test requirements for acceptance and
system testing.
The proposed software requirements and design specification techniques emerge from
integrating three categories of software specification languages, namely an infonnal
specification language (e.g. English), semiformal specification languages (Entity-Relationship
Diagrams, Data Flow Diagrams, and Data Structure Diagrams), and a formal specification
language (Z with an extended subset). The four specification languages mentioned above are
used to specify both software requirements and design. Both software requirements and design
of a system are defined graphically in Entity-Relationship Diagrams, Data Flow Diagrams, and
Data Structure Diagrams, and defined formally in Z specifications.
The proposed software requirements and design verification techniques are a
combination of informal and formal proofs. The informal proofs are applied to check the
consistency of the semiformal specification and to check the consistency, correctness, and
completeness of the formal specification against the semiformal specification. The formal
proofs are applied to mathematically prove the consistency of the formal specification.
Finally, the proposed technique for generating test requirements for acceptance and
system testing from the formal requirements specification is presented. Two sets of test
requirements are generated: test requirements for testing the critical requirements, and test
requirements for testing the operations of the system.