Systematic Transformation Method from UML to Event-B挂网链接：SRP:

https://www.scirp.org/book/detailedinforofabook?bookid=3046

亚马逊：

https://www.amazon.com/dp/1649979126?ref=myi_title_dp

谷歌图书：

https://books.google.cn/books/about?id=MoEMEQAAQBAJ&redir_esc=y

UML到Event-B的系统化转换方法（书２）20240330.docx

从20世纪60年代末期软件工程产生起，需求分析就一直是软件开发的重要主题。软件开发过程中，需要多方人员去配合来保障软件的稳定性和可靠性。根据软件开发过程中的形式化程度，可以把软件工程方法划分为非形式化、半形式化以及形式化三种。在面向对象的软件开发中，UML已经成为事实上的建模标准。然而，UML虽然直观容易理解和应用，却存在着不精确的语义，而且UML是一种半形式化的建模语言，无法进行形式化的验证。Event-B是一种基于大量数学谓词逻辑的形式化方法，虽然精确却难以理解和应用。因此，如何结合UML图和Event-B方法的优点是研究的重点。

以往的方法都是基于UML零散图到Event-B的转换，缺乏系统的转换方法。系统性的转换方法可以实现UML中的元素与Event-B中的元素相对应统一。一般的软件系统是中型系统，中型系统采用用例图、类图、状态图和顺序图这四种图就可以很好的表达清楚，有了上述的四种图，软件生命周期的需求获取、分析、设计、详细设计就可以完全表达清楚。本文以免疫系统和电梯系统为需求，采用Event-B形式化方法基于Rodin平台进行建模， 并在借助Rodin平台的证明器对模型进行了验证，通过ProB的动画模拟，iUML-B图形化前端以及BMotion Web展示了电梯模型事件的具体执行过程以及当前所处的状态，具体开展了如下工作：

第一，阐述了UML到Event-B的系统化转换方法，给出了UML用例图、类图、状态图和顺序图这四种图到Event-B形式化方法的转换规则，并给出了具体的实现过程。

第二，阐述了免疫系统中细胞免疫的作用机制，挖掘出细胞免疫的基本需求，基于Rodin平台为免疫模型进行建模，实现了细胞免疫到Event-B方法的转换，并对模型中产生的证明义务进行解除。 

第三、根据上述提到的转换方法，将该方法应用到对可靠性和安全性要求较高的电梯模型中。使用Rodin平台中自带的内部证明器以及Atelier B等提供的外部证明器对所建立的电梯模型进行验证。

第四，借助于iUML-B提供的图形化前端，BMotion Web的可视化功能以及ProB提供的动画模拟功能动态的模拟了模型中事件的执行过程，排除模型中死锁、不变量违规等问题，验证该转换方法的可行性和有效性。

总而言之，通过UML这四种图到Event-B的转换方法，以及对安全性和可靠性要求较高的电梯控制系统中的应用，基于该实例的研究，验证了UML到Event-B系统性转换方法的可行性和有效性。UML到Event-B的系统转换方法不仅增强了形式化方法的可理解性，有利于UML的精确化和软件从业人员的使用，而且有利于形式化方法的推广和应用。

关键词：Event-B；形式化方法；免疫模型；电梯模型；ProB；iUML-B

UML到Event-B的系统化转换方法（书２）20240330.docx