Research On Formal Architectural Semantics And Transformational Consistency Supporting Model Driven Development

Model-Driven Development (MDD) has become an active research area as well as a developmental trend of software engineering, which deals with the complexity of software development by raising the level of abstraction. Model transformation is a key technology in MDD, and the mapping relations between models are the foundation and basis for the transformation. However, most of the research on model transformations focuses on the description for model operations, which purpose is to achieve automatic transformations. There's currently no mature foundation on the definition of mapping relations as well as cardinal principles to evaluate the correctness and feasibility of transformation rules, which results in the status quo of the faultiness of the theory and realization of the MDD study, and makes model transformations can hardly meet the actual demands.The correctness of model transformations is a key issue of model-driven engineering, which also is the core problem of all researches on model-driven approaches. The general criteria about the correctness of model transformations comprise syntactic correctness, syntactic completeness, termination, confluence and semantic consistency. There have already been comparatively mature solutions for the judgment of these criteria with the exception of semantic consistency. However, there are currently no mature theoretical foundations and verification tools on the analysis and judgment about semantic consistency of model transformations. The definition, description, and proof of semantic property preservation of model transformations are still problems unresolved. How to ensure semantic consistency between the models before and after transformation has become a key issue on the road of MDD becoming more mature. Many researchers believe that the current descriptions of high-level models of MDD are neither complete nor accurate for lacking understandable formal semantic meanings, which makes it difficult to achieve correct model transformations and code generations, and also leads to a very limited evaluation on transformation tools. All the facts show that, the lack of description and calculation approaches for semantic properties currently is the main lacking theory of model driven software development, and to build a theory for semantic description and calculation becomes the basis and urgency for its healthy and rapid development.Many years of practice and the test of markets at home and abroad show that, the combination of software architecture and MDD has been successful in software rapid development, varying on demand, quality assurance and cost control, and has high values in practical application. Based on the application background and demands mentioned above, and in order to resolve the problems of the basic theory and technology of model transformations, this dissertation absorbs the research results of the field of software architecture and the field of formal methods in software engineering, and then makes a deep research on the processes and approaches of model transformations. Especially, this dissertation focuses on the formal semantic description of architecture models and their mappings. On this basis, the semantic properties that should be preserved through model transformations are discussed subsequently. A prototype system tool is also built in the study to apply and validate the research results. The main research contents and innovations of this dissertation are as follows:(1) The process and approaches of model transformations are studied. Starting from the analysis of modeling languages, this dissertation discusses the requirements of semantic consistency of model transformations and model mappings, and summarizes and classifies the processes and approaches of model transformations. With help of the mechanism of formalism extensions, a concept-reconstruction based model mapping approach is proposed. On this basis, a further study is conducted to explore the definition process for mapping relations between different modeling languages and the cardinal principles should being followed. Then, this dissertation puts emphasis on the analysis of the definition of mapping relations and the constructing processes of transformations between structural models at different levels of abstraction. A theoretical framework of architecture-mapping based model transformation is proposed based on the abstract definition of architecture models, and thus lays the theoretical foundation for the further study on the consistency of architecture-based model transformations.(2) A description framework is built for the formal semantics of architecture models and their mappings. In this dissertation, the typed category theory proposed by professor Lu Ruqian (an academician of Chinese Academy of Sciences) is extended and combined with algebraic specification and process algebra to provide a unified description framework for the formal semantics of architecture models and their mappings. The structural semantics of architecture models are described within typed category diagrams, and the behavioral semantics are represented by process traces affiliated to the categorical framework, and the mapping relations between component models are formally described by morphisms and functors of category theory. The describing mechanism is generic enough for more situations, and the mapping description can be accomplished through a series of small and local mappings of which the results can be combined to form a larger composite architecture, i.e., the mapping from an abstract model to a concrete implementation is described in an incremental way. Thereby, a feasible idea and method is provided for the combination of local mappings. Another advantage of using category theory as a mathematical framework to formalize software architectures is that the questions themselves can be formalized and resolved in terms that are independent of any specific application domain. Category theory supports the diagrammatic representation of component models that visualizes the relationships between components and the structural features, which can be used to strengthen the understandability and traceability of model transformations. The application research shows that the description framework commendably captures the essence, process and requirements of model-driven development, and thus can be used as a new theoretical guidance for the cognition, design and semantic calculation of model transformations and model-driven development. This dissertation is the first report in which the typed category theory has ever been used to study the organizational structure of models and the mapping relations between them. It will provide a new way of thinking for the researchers on the transformations between software models. (3) The semantic properties that should be preserved through model transformations are studied. The semantic transfers arising in architecture model transformations are analyzed and discussed firstly. Then, based on the formal semantics of architecture models, the problems of the definition and description of semantic property preservation of model transformations are analyzed from the aspects of structural semantics, axiomatic semantics, portal semantics and behavioral semantics, and the corresponding criteria are also given respectively. At the same time, the approaches to prove whether a transformation satisfies some preservation constraints are discussed, which enable verification of property preservation in the way of theorem proving, and thus overcome the shortcomings of model checking. The work does not only provide a theoretical guidance for the definition of transformation rules, but also provide a measure for the validation of mapping relations between models at different levels of abstraction, and thus lays the foundation for the further full study on the principles should being followed and the properties should being preserved through model transformations. This is the first time that the correctness of model transformation is proposed to be judged from the viewpoint of semantic consistency of model compositions which are expressed by the mapping relations between architecture models. The research work is a new attempt in the field of model-driven software development.(4) For the aspects of development and application, a prototype system tool for model driven approach has been developed, and has been applied into engineering. Starting from software architecture modeling, a modeling approach has been proposed to build high level models for Web applications by extending UML, which comprises architecture model, static view, logic view and UI presentation view. Then, according to the theory and methods of the research on architecture-centric model transformations, the mapping relations and transformation rules have been defined. J2EE and ASP.NET have been used as two target platforms to achieve model transformations as well as code generations, and thus the theory and methods of this dissertation is verified.The results of this dissertation enrich and improve the theoretical foundation of MDD approaches, and provide a new idea for the researchers on model-driven software development. It plays an important and positive role for the promotion of the stable and fast growing of MDD, for the elevation of levels of software development and for the enhancement of development efficiencies. The framework for semantic description enriches the studies on formal methods of software architecture, and promotes the application and development of category theory in computer science, and provides a reference and inspiration for the researchers engaged in the field of category theory. Further more, the work will be conducive to the development of intelligent software, for the typed category theory meets the need of abstract knowledge description and knowledge processing, and has representational and inferential power.