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

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

来源：计算机技术与发展, 2023, 33(12): 113-120.

• 统一建模语言
• 形式化方法
• Event-B
• 抽象转换
• 模型

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