Higher-order Refinement Techniques for Model Driven Architecture

Enterprise software applications increasingly drive most aspects of modern business. These systems are inherently complex and heterogeneous - they involve the integration of different business perspectives, implemented across a suite of middleware and platforms. The challenge is to develop methods to implement this integration in a way that leads to robust and trustworthy enterprise systems.Model Driven Architecture.Model Driven Architecture (MDA) is targetted at this issue / and is a way of integrating and developing systems from heterogeneous system models.It is receiving significant attention from industry - major players such as IBM, Oracle and Rational Software are actively supporting MDA standards developed by the Object Management Group (OMG).The key idea behind MDA is to first develop platform independent models, and then use transformations to refine to specific platforms and architectures. The platform independent models provide abstract architectural and process specifications of systems, independent of the choice implementation technologies. The transformations define how platform independent models (e.g., written in UML) are implemented on the middleware and platforms of a particular enterprise.The benefit of MDA is that designers can focus on providing robust and architecturally sound business models at a suitable level of abstraction. Crucially, for MDA to be successful in practice, support for automating the transformations to the individual platforms must be provided.Model transformations.MDA has the potential for a wide impact across industry - initial industrial applications have shown system development time being improved by a factor of 10 through the use of MDA techniques.The MDA is an OMG standard that builds upon the success of UML. There is already significant uptake of the method from within the enterprise software engineering sector, and there is a real opportunity to promote a software development approach that emphasizes the advantages of modelling at various levels of abstraction and develops tools and techniques to support this.However, MDA remains an essentially informal approach, and work is needed on generic and uniform ways of developing and implementing such transformations. In addition, current techniques do not guarantee correctness of the model transformations, and make it difficult to deal with inconsistencies, error propagation and error detection.This project addresses the important question of how to develop and implement correct MDA transformations.We will do this byformalising MDA metamodels: to provide provide a common framework for the MDA architecture and its model transformations;providing a way to develop model transformations: to obtain a toolkit to specify and synthesize complex model transformations that are provably correct with respect to their specification;developing tool support: that implements our methods, supports the OMG standards and is interoperable with commonly used MDA CASE tools.Delivering this presents us with some serious research issues:how to encode the MDA model hierarchy;how to use this to develop automatic transformations; and how toimplement these so that as much of the theory is hidden from the user as possible.The MDA model hierarchy is intrinsically higher-order, and requires an expressive formal framework from which we can synthesize complex model transformations. However, expressivity must be balanced with computational power, and a constructive approach is necessary. To do this we will bring together constructive type theory, refinement and transformation techniques with support for automated deduction. Such an approach has a sound semantic underpinning and the domain of application offers the opportunity for the well-founded and effective engineering of tool support.