摘要：

Event-B共享变量和共享事件方法可将大型系统分解成多个子系统,并独立建模开发,但其需要手工干预以实现模型间事件的组合。为提高组合效率,提出一种针对模型的自动化组合理论,并开发自动化组合工具原型。为在精化模型中逐步引入模块调用,改进PROG方法,开发自动精化工具原型。通过2个应用案例,验证了自动化组合工具能自动组合事件,自动精化工具能减少调用变量的数量,从而增强系统模型的可读性和可维护性。

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

Abstract:

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.

Key words: formal method, Event-B method, modular modeling, automated module composition method, module calls, refinement

中图分类号: 

• TP274