Formal method integration via heterogeneous notations

grantor: University of TorontoMethod integration is the procedure of combining multiple methods to form a new technique. In the context of software engineering, this can involve combining specification techniques, rules and guidelines for design and implementation, and sequences of steps for managing an entire development. In current practice, method integration is often an ad-hoc process, where links between methods are defined on a case-by-case basis. In this dissertation, we examine an approach to formal method integration based on so-called heterogeneous notations: compositions of compatible notations. We set up a basis that can be used to formally define the meaning of compositions of formal and semiformal notations. Then, we examine how this basis can be used in combining methods used for system specification, design, and implementation. We demonstrate integration using this basis in a pure formal setting, and in a setting involving both formal and semiformal methods. This culminates in a description of a meta-method for formal method integration based on heterogeneous notations, and a discussion of the properties and benefits obtained through the use of such a method. A number of examples are provided that suggest how heterogeneous notations and integrated methods can be used, and how formal method integration based on the meta-method can occur.Ph.D