|
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的系统化转换方法(书2)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的系统化转换方法(书2)20240330.docx
Archiver|手机版|科学网 ( 京ICP备07017567号-12 )
GMT+8, 2024-9-28 06:13
Powered by ScienceNet.cn
Copyright © 2007- 中国科学报社