Formal specification-based monitoring, regression testing and aspects

Abstract

With the sound mathematical basis and well-defined semantics and syntax of formal languages, the formal specification of a software system provides deep insight into and precise understanding of system requirements. It also provides a powerful basis for software verification and validation. This thesis explores parts of the potential of formal specifications in contributing to high quality software. A formal specification-based software monitoring approach is proposed in this thesis. Based on formal specification animation and program debugging, the proposed software monitoring approach dynamically and continuously checks the conformance of concrete implementations to formal specifications, explicitly recognizes undesirable behaviors in the target system, and responds appropriately in a timely manner as the target system runs. Frequently, the formal specification of a software system has to change according to the changes of system requirements. Correspondingly, the implementation of the software system has to be changed in order to keep conformance with the formal specification. Taking advantage of aspect-oriented programming technique, we propose an approach for handling the evolution of core classes in object-oriented programs when the formal specification of a system has changed. After the software has evolved according to the changes of the formal specification, regression testing has to be performed to ensure that the changed parts of the software behave as intended and that the unchanged parts have not been adversely affected by the modifications. To reduce the cost of regression test and deal with the conditions that cannot be handled by code-based regression test selection techniques, a formal specification-based regression test suite construction approach is proposed in this thesis. Aspect-oriented software development (AOSD) is a new promising methodology. However, validation techniques for aspect-oriented programs are still far from sufficient. With the expectation that formal methods could be applied to aspect-oriented programs in the future, we extend the integrated formal notation Timed Communicating Object-Z (TCOZ) with the mechanisms for formally specifying those aspect-oriented constructs, providing a starting point for future research work on the development of formal methods for aspect-oriented software development.