【作者】 侯金奎；

【导师】 王海洋；

【作者基本信息】 山东大学 ， 计算机软件与理论， 2008， 博士

【摘要】 模型驱动开发(Model-Driven Development,MDD)已成为软件工程技术的研究热点和发展趋势,它通过提升抽象层次来应对软件开发的复杂性。模型转换是MDD方法中的一项关键技术,模型间的映射关系是模型转换的基础和依据。但目前关于模型转换的研究成果大都集中在模型操作的描述方面,其目的是实现转换过程的自动执行,而在映射关系的定义原则,以及转换规则的可行性和正确性验证等方面,还缺乏坚实的理论基础,从而导致了MDD研究的理论和实现不完善,模型转换难以满足实际需要的现状。模型转换的正确性问题是所有基于模型驱动的软件工程实施的基础问题,也是模型驱动开发研究的核心问题。模型转换正确性的一般标准包括语法正确性、语法完备性、可终止性、合流性和语义一致性。在这几个转换标准的判定上,除语义一致性外,其它几个语法层次上的正确性问题都已有相对成熟的解决方案。而在模型转换的语义一致性验证和分析方面,目前还没有成熟的理论基础和验证工具,模型转换中语义特性保持的定义、描述和验证仍是一个尚未解决的难题。如何保证模型转换前后的语义一致性,是模型驱动方法走向实现的关键。但在目前的MDD实现方法中,形式化语义的缺乏使得高层模型的描述还不够完备、精确,难以有效的支持模型转换和代码生成,也不能建立有效的评价和验证机制。缺乏模型转换相关的语义特性描述和计算,是当前基于MDD的软件开发研究中所缺乏的主要理论。建立模型转换相关的语义描述和计算理论是促进MDD方法健康快速发展的基础和当务之急。国内外多年的实践和市场的验证表明,软件体系结构和MDD的结合在软件的快速开发、随需应变、质量保证以及成本控制等方面是成功的,有很好的发展前景。基于以上的应用背景和需求,本文立足于解决模型转换的基础理论和技术问题,吸收软件体系结构和软件形式化等方面的研究成果,在对模型转换过程和方法进行深入研究的基础上,重点研究了软件体系结构模型及其间映射关系的形式化语义描述,以此为基础,对模型转换应保持的语义特性进行了分析和探讨,并开发了原型系统对研究成果进行了应用和验证。本文主要的研究内容和创新工作包括:(1)对模型转换过程和方法的研究。从模型描述语言的分析入手,讨论了模型转换和模型映射的一致性需求,并对模型转换的过程和已提出的模型转换方法进行了综述和归结。借助于形式语言的扩展机制,提出了基于概念集重构的模型映射定义方法,讨论了模型描述语言之间映射关系的建立过程以及所应遵循的基本原则,并重点分析了不同抽象层次结构模型之间的映射关系定义和转换的构造过程。依据体系结构模型的抽象定义,提出了基于体系结构映射的模型转换理论架构,从而为基于软件体系结构的模型转换一致性研究奠定了理论基础。(2)建立了体系结构模型及其映射关系的形式化语义描述方法。在对陆汝钤院士提出的类型范畴理论进行扩展的基础上,将其与代数规范和进程代数相结合,为软件体系结构模型以及模型间的映射关系提供了一种统一的语义描述框架。模型的结构语义由类型范畴图表来指代,行为语义则由范畴附带的进程行为迹来表示,模型间的映射关系用范畴理论中的态射和函子来形式化描述。该描述机制通用性强,通过将一系列小的局部映射的结果组合在一起形成大的复合结构,以一种渐增的方式来描述抽象模型到具体实现的转换关系,从而为局部映射的组合提供了一种可行的思路和方法。使用范畴理论作为数学框架,使得所讨论的问题可以用与特定应用领域无关的术语来形式化描述。范畴理论支持图形化建模,可以使模型中的构件关系以及结构特征可视化,有利于对模型转换的理解和追踪。应用研究表明,该描述框架很好地把握了模型驱动开发的实质、过程和要求,为模型转换和模型驱动的软件开发提供了新的认知、设计和语义计算的指导架构。本文是首次将类型范畴理论用于研究模型的组织结构和模型间的转换关系,将为其他学者研究软件模型的转换问题提供一种新的思路。(3)对体系结构模型转换所应保持的语义特性进行了研究。分析了模型转换过程中的语义迁移。基于软件体系结构模型的形式化描述,从结构语义、公理语义、端口语义和行为语义等几个方面分析了模型转换中特性保持问题的描述,并建立了相应的判定标准,同时探讨了证明一个转换是否满足某些特性保持约束的方法。这些方法支持以定理证明的方式,对模型转换的语义特性保持进行验证,克服了模型检测的不足。该研究可用于指导模型转换规则的定义,为模型映射关系的正确性验证提供依据,从而为进一步全面研究模型转换所应遵循的法则和特性奠定基础。本文是首次提出从体系结构模型之间的映射关系所表达的模型复合的语义的一致性来考察模型转换的正确性,在模型驱动开发研究领域是一次新的尝试。(4)在开发和应用方面,开发了模型驱动方法的原型工具,并完成了一系列的工程应用。从软件体系结构建模出发,通过对UML进行扩展,提出了一种包括体系结构模型、静态视图、逻辑视图和界面展示视图四部分的WEB应用模型描述方法。然后依据体系结构模型转换一致性研究的理论和方法定义模型转换规则,实现了向J2EE平台和ASP.NET平台的模型转换和代码生成,从而验证了本文所提理论和方法的合理性和实用性。本文的研究成果丰富和完善了MDD方法的理论架构,为模型驱动的软件开发研究提供了一种新的思路,对于促进MDD方法坚实、快速的发展,提升软件开发层次和提高开发效率,有重要和积极的推动作用。本文提出的语义描述框架丰富了软件体系结构形式化方法的研究,推动了范畴理论在计算机科学中的应用和发展,可以为从事范畴论方向的研究人员提供参考与启发。另外,类型范畴理论适合知识的抽象描述和知识处理,并且具备表达和推理能力,本文的工作还将有利于智能开发软件的研究。更多还原

【Abstract】 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.更多还原