UML 到 Event-B 的系统化转换方法

来源：计算机技术与发展杂志2023年第12期北京时间：

作者：耿雪;邹盛荣*;刘晓莹;姚聚义

单位：扬州大学 信息工程学院,江苏 扬州 225009 Author(s): GENG Xue;ZOU Sheng-rong* ;LIU Xiao-ying;YAO Ju-yi School of Information Engineering,Yangzhou University,Yangzhou 225009,China 关键词: 统一建模语言;形式化方法;Event-B;抽象转换;模型 Keywords: unified modeling language ( UML) ;formal method;Event-B;abstract transformation;model 分类号: TP311 DOI: 10. 3969 / j. issn. 1673-629X. 2023. 12. 016 摘要: 在面向对象的软件开发中,UML 已经成为事实上的建模标准。 然而,UML 虽然直观容易理解和应用,却存在着不精确的语义,而且 UML 是一种半形式化的建模语言,无法进行形式化的验证。 Event-B 是一种基于大量数学谓词逻辑的形式化方法,虽然精确却难以理解和应用。 因此,如何结合 UML 图和 Event-B 方法的优点是研究的重点,以往的方法都是基于 UML 零散图到 Event-B 的转换,缺乏系统的转换方法。 系统性的转换方法可以实现 UML 中的元素与 Event-B 中的元素相对应统一。 一般的软件系统是中型系统,中型系统采用用例图、类图、状态图和顺序图这四种图就可以很好地表达清楚,有了上述的四种图,软件生命周期的需求获取、分析、设计、详细设计就可以完全表达清楚。 文章中分别给出了这四种图到 Event-B 的转换方法,并将该系统的转换方法应用到对安全性和可靠性要求较高的电梯控制系统中。 基于该实例的研究,验证了 UML 到 Event-B 系统性转换方法的可行性和有效性。 UML 到 Event-B 的系统转换方法不仅有利于 UML的精确化和软件从业人员的使用,而且增强了形式化方法的可理解性,有利于形式化方法的推广和应用。 Abstract: In object-oriented software development,UML has become a de facto modeling standard. However,although UML is easy tounderstand and apply,it has inaccurate semantics,and?UML? is a semi - formal modeling language,which cannot be formally verified.Event-B is a formal method based on a large number of mathematical predicate logic,which is precise?but difficult to understand andapply. Therefore,how to combine the advantages of UML diagram and Event-B method is the focus of the research. The previous transformation methods are based on the transformation from UML scatter diagram to Event - B,, and lack of systematic transformationmethods. The systematic transformation method can realize the unity of elements in UML and elements in Event - B. Medium - sizedsystem can be clearly expressed by using use case diagram,class diagram,state diagram and sequence diagram. With the above four diagrams, the requirements acquisition,requirement analysis,design and detailed design of the software life cycle can be fully expressed.Based on the elevator case study,the feasibility and effectiveness of the system transformation method from UML to Event-B proposedare verified. The system transformation method from UML to Event-B not only improves the accuracy of UML and is easy for softwarepractitioners to use,but also enhances the comprehensibility of formal methods and is conducive to the promotion and application offormal methods.

摘要：在面向对象的软件开发中,UML 已经成为事实上的建模标准。 然而,UML 虽然直观容易理解和应用,却存在着不精确的语义,而且 UML 是一种半形式化的建模语言,无法进行形式化的验证。 Event-B 是一种基于大量数学谓词逻辑的形式化方法,虽然精确却难以理解和应用。 因此,如何结合 UML 图和 Event-B 方法的优点是研究的重点,以往的方法都是基于 UML 零散图到 Event-B 的转换,缺乏系统的转换方法。 系统性的转换方法可以实现 UML 中的元素与 Event-B 中的元素相对应统一。 一般的软件系统是中型系统,中型系统采用用例图、类图、状态图和顺序图这四种图就可以很好地表达清楚,有了上述的四种图,软件生命周期的需求获取、分析、设计、详细设计就可以完全表达清楚。 文章中分别给出了这四种图到 Event-B 的转换方法,并将该系统的转换方法应用到对安全性和可靠性要求较高的电梯控制系统中。 基于该实例的研究,验证了 UML 到 Event-B 系统性转换方法的可行性和有效性。 UML 到 Event-B 的系统转换方法不仅有利于 UML的精确化和软件从业人员的使用,而且增强了形式化方法的可理解性,有利于形式化方法的推广和应用。

关键词：统一建模语言;形式化方法;Event-B;抽象转换;模型