信息物理融合系统是信息世界和物理世界高度融合和深度协作的新型工业系统,被美国政府列为未来八大关键信息技术的首位。它采用计算智能、通信和控制深度融合的3C结构,实现计算过程与物理过程相融合,系统不仅包含离散的计算过程,还涉及连续物理事件的处理,形成网络、控制与嵌入式系统的动态重组与整合。信息物理融合系统具有状态感知、实时通信、信息计算、精准控制以及自主协调等丰富能力,改进了工业系统的稳定性、可靠性、鲁棒性和工作效率等多项关键性能指标,从而全面地促进工业经济发展和提升了社会综合效益。因为信息物理融合系统对生产生活深度融入,所以如果它出现问题将可能会带来不可估量的生命和财产损失,因此它对安全性和可靠性有着更高的要求。与一般传统系统相比,信息物理融合系统具有高度的混成性、复杂性以及更高的安全要求,这些需求给设计开发这类系统带来了更大的挑战。如何建立可信的信息物理融合系统是国内外工业界和学术界的难题之一。在计算机科学领域里,Event-B精化开发被认为是一种开发复杂系统的有效形式化方法,已经有许多成功的开发实例。虽然Event-B方法提供了一套完整的精化开发系统的机制,但该机制只适用于离散系统。而信息物理融合系统含有物理实体的连续状态,该传统方法已不再奏效。针对具有混成特性的信息物理融合系统,我们以Event-B精化开发框架为基础,继承Event-B的优良特性,提出一种Hybrid EventB语言。它以Event-B为基础,具备对连续实时行为进行建模、精化的正确性证明能力。考虑到混成系统的多样性,我们借鉴经典的混成自动机的模型机制,提出一种新的微分事件类型来扩展Event-B语言的machine结构,保证新的模型语言具有较强的建模能力,能够建模更多形式的混成系统。Event-B通过证明一系列内设的证明义务规则,确认模型的正确性。针对新的微分事件,根据微分事件语义和事件模型的正确性与一致性的要求,我们建立了微分事件的证明义务规则,这些规则为正确开发混成系统提供了保证。由于微分事件内采用了微分方程对连续行为进行了建模,我们提出并论证了一种采用微分不变量技术,可不求解微分方程的证明义务的证明方法,实现证明义务的证明,并将Rodin工具和KeYmaera工具整合在一起作为支持工具。我们以轨道交通系统作为实际案例,显示Hybrid Event-B能够较好完成混成系统的精化开发。我们以Event-B精化开发理论为基础,提出了Hybrid Event-B建模与精化方法。本文主要从建模、证明义务、验证技术和验证工具等四个方面开展研究,提出了一个全面的精化开发信息物理融合系统的方案。主要内容:·针对信息物理融合系统中混成行为的建模需求,扩展Event-B语言提出一种新型建模语言Hybrid Event-B。该语言除了采用传统事件建模离散行为,还引入一种以微分动力系统为基础的新型事件微分事件,用来建模系统的连续行为。同时继承学习了混成自动机的离散与连续的交互机制,实现离散事件和微分事件间交互。该部分的研究为信息物理融合系统的精化开发提供了建模方法。·给出了Hybrid Event-B模型的证明义务。证明义务是Event-B精化开发方法中一些预设的规则,通过规则的证明确认模型的正确性。依据Floyd断言理论、Hoare逻辑及精化理论,为Hybrid Event-B提出了不变量、可靠性及精化等证明义务,为信息物理融合系统的精化开发提供了正确性验证依据。·提出并论证了基于微分不变量的证明义务证明技术。Hybrid Event-B的微分事件采用微分方程建模连续行为,基于状态集验证方法需要近似或精确求解微分方程,存在求解困难的问题。使用微分不变量技术可在不求解微分方程的情况下,验证证明义务。在精化开发中使用微分不变量技术,是一项非常重要的技术和理论贡献,它有效地提升了精化开发信息物理融合系统的适用范围和实用性,也拓展了微分不变量理论的应用领域。·探索了将Rodin平台扩展及同KeYmaera平台结合的工具方案。工具支持是精化开发实用化的重要步骤。Rodin是传统Event-B的具有可扩展性的工具平台,通过分析Rodin平台的工作机制与接口特点,将Hybrid Event-B的新增模型元素添加到Rodin平台中,并把Rodin中需要证明的微分事件的证明义务转换成KeYmaera定理证明器的输入,实现和KeYmaera定理证明器的整合完成验证工作。