A framework for verification of SDL software specifications

Formal verification of hardware designs is a well established practice. Formal verification of software designs is not as readily embraced due to the fact that the methodologies for formal software verification are not integrated into the software design cycle. The need for formal verification in an industrial setting is clearly demonstrated by the small scale verification efforts within individual software construction projects and the construction of the CASE tools that aim to support the application of formal methods. This dissertation introduces an approach to formal verification of software specifications that fits seamlessly into the design cycle. The approach includes verification and simulation capabilities for specifications and the testing capabilities of implementations of the specifications. Benefit of application of formal methods are maximize through the use of verification artifacts as a test harness and a test oracle during the testing stage.; The approach is applied to specifications recorded in the SDL formal description language. The ACL2 theorem prover is used as the underlying reasoning system. The ACL2 feature that allows to both reason about a model of a specification and to execute it is exploited in this work. A simulator for SDL specification, the cornerstone mechanism of the approach, is constructed and shown to be correct. The simulator allows explicit network handling and implements several versions of granularity of execution of SDL transitions. Several correctness properties of the simulator are identified and proved in collaboration with ACL2. The proved properties include the preservation of well-formedness of internal constructs and properties derived from the operational semantics of SDL. Mechanical means of checking correctness are designed for cases where construction of formal ACL2 proofs is impractical.