UML到Event-B的系统化转换方法
Systematic Transformation Method from UML to Event-B
耿雪 1邹盛荣 1刘晓莹 1姚聚义1
作者信息
- 1. 扬州大学 信息工程学院,江苏 扬州 225009
- 折叠
摘要
在面向对象的软件开发中,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 to understand 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 and apply.Therefore,how to combine the advantages of UML diagram and Event-B method is the focus of the research.The previous trans-formation methods are based on the transformation from UML scatter diagram to Event-B,,and lack of systematic transformation methods.The systematic transformation method can realize the unity of elements in UML and elements in Event-B.Medium-sized system 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 proposed are verified.The system transformation method from UML to Event-B not only improves the accuracy of UML and is easy for software practitioners to use,but also enhances the comprehensibility of formal methods and is conducive to the promotion and application of formal methods.
关键词
统一建模语言/形式化方法/Event-B/抽象转换/模型Key words
unified modeling language(UML)/formal method/Event-B/abstract transformation/model引用本文复制引用
出版年
2023
国家科技期刊平台
NSTL
维普
万方数据