The Unified Modeling Language (UML) is an important part of Modeling-driven engineering (MDE) because of its variety of well-known and intuitive graphical notations.However,the semantics of UML is not precisely defined and the correctness of refinements cannot be verified,which makes it difficult to verify in formal of the UML model.As the static model of describing system structure,UML class diagram has no complete formal semantics.Thus,using the theorem proof assistant Coq to formalize and mechanize the semantics of the UML class diagram and the refinements between the models.The syntactic structure and the semantics of the UML class diagram can be transformed to the rigorous definitions in Coq,which is called mechanized semantics.Besides,the structural refinement operations of the class diagram are also provided.The refinement relations between models can be formally defined in Coq,and the desired properties of the refinement relations can be proven to verify the correctness of the refinements,ensuring the consistency of structure and semantics before and after refining.Combining the UML and formal method,the theoretical foundation in the software developing process is provided.%UML由于其广泛的应用和直观的图形化符号,成为了模型驱动工程的重要组成部分.但UML本身缺乏精确的形式语义定义,缺少对其模型精化关系的形式化规范定义,对UML模型进行形式验证变得尤为困难.UML类图作为描述系统结构的静态模型,不具备完整的形式语义.从UML类图的机械语义中抽取出形式规约,将UML类图中的结构和形式规约转换成定理证明器Coq中的机械语义定义.此外,还提出了类图的结构精化操作,将模型间的精化关系在Coq中进行形式化定义,并且对精化操作的原子操作进行机械验证,保证其精化前后系统的结构和语义保持一致.将UML和形式化方法相结合,为可验证的软件设计精化框架提供了理论依据.
展开▼
