基于时序约束建模的自动精化和组合工具

Automatic refinement and combination tools based on timing constraint modeling

为提供更优质的使用Event-B形式化方法建模混合系统的工具,根据混合系统的时序约束建模方法,其能够很好刻画混合系统建模中的时间相关性质并且支持精化和组合,提出基于它的自动筛选、精化和组合的方法。开发对应的自动精化和组合的工具链,工具链包含模型检测、自动精化和组合、模型证明等一系列功能并拥有用户友好的界面。给出一个使用工具的案例介绍和应用此工具。

To provide better tools for modeling hybrid systems using Event-B formal methods,according to the timing constraint modeling method of the hybrid system,which can well describe the time-dependent properties of the hybrid system modeling and support refinement and combination,a method of automatic screening,refinement,and combination was proposed.A corresponding automatic refinement and combination tool chain was developed as well.The tool chain included a series of functions such as model detection,automatic refinement and combination,and model verification,and it has a user-friendly interface.A case study of using the tool was shown to introduce and apply this tool.