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.