基于Event-B的自动化模块组合方法研究  

Research on Automated Module Composition Method Based on Event-B

作　　者：陈金鑫 苏雯 CHEN Jinxin;SU Wen(School of Computer Engineering and Science,Shanghai University,Shanghai 200444,China)

机构地区：[1]上海大学计算机工程与科学学院,上海200444

出　　处：《计算机工程》2019年第5期298-307,314,共11页Computer Engineering

基　　金：国家自然科学基金(61602293)

摘　　要：Event-B共享变量和共享事件方法可将大型系统分解成多个子系统,并独立建模开发,但其需要手工干预以实现模型间事件的组合。为提高组合效率,提出一种针对模型的自动化组合理论,并开发自动化组合工具原型。为在精化模型中逐步引入模块调用,改进PROG方法,开发自动精化工具原型。通过2个应用案例,验证了自动化组合工具能自动组合事件,自动精化工具能减少调用变量的数量,从而增强系统模型的可读性和可维护性。Event-B shared-variable and shared-event methods can decompose a large scale system into multiple subsystems and model them independently.Nevertheless,the existing Event-B method requires manual intervention to perform event composition among models.Therefore,this paper proposes a theory for the automated composition of models and develops an automated tool to improve the efficiency of model composition.With regard to the step-by-step introduction of module calls in the refinement model,this paper improves the PROG method and develops an automated refinement tool prototype.Through the two application case,the automated composition tool can compose events automately,the refinement tool reduces the call variables,which enhances the readability and maintainability of the system model.

关 键 词：形式化方法 Event-B方法 模块化建模 自动化模块组合方法 模块调用 精化 

分 类 号：TP274[自动化与计算机技术—检测技术与自动化装置]