| As software grows more complex, the difficulty of ensuring its behavioral correctness becomes much more difficult. Furthermore, we are placing software systems in safety critical applications, such as power plants, airplane control systems, defense and medical devices. Deployed failures in these systems are both life threatening and potentially expensive for negligent software developers. Thus, additional effort in testing the software to provide high quality assurance is justified.;One of the central problems with testing these critical systems is verifying behavioral correctness of test executions. Typically, the test results are checked manually, which is tedious and error-prone. Using a formal specification, which is a system description in a language that has well defined semantics, behavioral correctness can be verified automatically. Formal specifications also support testing early in the development lifecycle, before the design or implementation have been started.;This dissertation describes the Execution-time Analysis for Specification-based Oracle Failures (EASOF) model for specification-based testing and instantiations of the generic model for an implementation language and two specification languages. The model supports features such as multi-lingual specifications, whereby a system specification is composed of multiple sub-specifications, each specifying some aspect of the system and written in the most appropriate specification language; representation mappings, which allow a non-trivial relationship between the implementation and specification; implementation instrumentation, which captures the internal state of the implementation; and test oracle engines, which verify execution behavior with respect to specifications. Two examples demonstrate the application of the model and the use of supporting tools.;The most significant contribution of this model of specification-based testing and the dissertation is generic support for automated general specification-based test oracles through test oracle engines. Test oracle engines provide a procedure for comparing test execution behavior traces to a specification in any supported specification language. These oracle engines are more efficient than direct interpretation of the specification, because the model supports transformations of the specification to efficiently checkable forms. |
