摘要
在面向对象的软件开发过程中,UML被广泛应用于建模,但因其语义的不精确性使得模型难以进行形式化验证。同时,Event-B作为一种基于数学逻辑的形式化方法,尽管精确但难以理解。为了充分发挥两种方法的优势,提出一种将UML与Event-B形式化方法相结合的解决方案,针对中型Web应用系统,提出了用例图、类图、顺序图、组件图和部署图5种UML图到Event-B的转换方法。通过将其应用于实际Web应用系统,并利用Rodin平台的证明器解除模型中的证明义务,验证了这一转换方法的可行性和有效性。该方法的应用,不仅提高了UML的精确性和系统的可靠性,减少了故障风险,还增强了形式化方法的可理解性,有助于其推广和应用。
In the process of object-oriented software development,UML is widely used in modeling,but because of its semantic imprecision,it is difficult to verify the model formally.At the same time,as a formal method based on mathematical logic,Event-B is accurate but difficult to understand.In order to give full play to the advantages of the two methods,a solution combining UML and Event-B formal methods is proposed.For medium-sized Web application systems,five UML diagrams to Event-B conversion methods are proposed,including use case diagram,class diagram,sequence diagram,component diagram and deployment diagram.By applying these methods to the actual Web application system and using the prover of Rodin platform to release the proof obligation in the model,the feasibility and effectiveness of this transformation method are verified.The application of this method not only improves the accuracy of UML and the reliability of the system,reduces the risk of failure,but also enhances the comprehensibility of the formal method,which is helpful to its promotion and application.
作者
智玉华
邹盛荣
刘晓莹
耿雪
ZHI Yuhua;ZOU Shengrong;LIU Xiaoying;GENG Xue(School of Information Engineering,Yangzhou University,Yangzhou 225009,China)
出处
《软件导刊》
2025年第8期112-120,共9页
Software Guide
