王烨凯，苏 雯

(上海大学 计算机工程与科学学院，上海 200444)

0 引 言

混合系统[1]是一个日益重要的新兴领域，它经常出现在汽车工业、航空、工厂自动化等领域。Event-B[2]是基于集合和一阶谓词逻辑的形式化系统开发方法，将混合系统进行Event-B形式化建模很好地解决其复杂的系统设计的方法。在使用Event-B方法的建模的工具支持上，Abrial等开发了Rodin平台为Event-B方法提供了开发建模的基础平台。许多学者为Rodin平台扩展了功能，如UML-B[4]工具提供了图形化建模功能；EventB2 Java[5]工具提供了Event-B语言转化成Java语言的工具；事件精化结构工具[6]为事件精化结构方法提供了工具支持；特征组合工具支持“特征”的组合和重用等等，在精化和组合的工具支持上都仅针对于特定方法进行辅助。由于时间约束问题的对于混合系统建模的重要性，文献[3]对现有的Event-B混合系统建模方法进行改进，提出基于混合系统的时序约束建模方法，可以很好地刻画混合系统中的时间约束问题并支持混合系统时间约束的精化和组合。现有的工具需手工参与多，难以辅助自动化开发，因此需要有针对时间约束的混合系统模型自动精化和组合的工具。为此我们先提出了基于混合系统时序模型的自动精化和组合方法，然后开发了基于该方法的混合系统时序模型的自动精化和组合的工具。工具提供了一个用户友好的操作界面，并且拥有自动化性能，使用户可以用最少的操作实现功能。工具在保证模型正确性的前提下，能够根据自行精化和组合方法形成的规则库，对模型进行快速的精化和组合。……