混成系统是近些年来学术研究的热点领域之一，其主要特征表现为物理进程和计算进程的深度融合，广度交互，混成系统的异构性、复杂的时间约束性、一定的时间可预测性、更高的安全性以及交互的复杂性和不可预测性，给这类系统的描述、设计、分析和验证带来了巨大的挑战。如何保证信息物理融合系统的正确性业已成为国内外工业界和学术界的难题之一。本项目发展了一种混成系统的建模语言和基于事件的建模方法，引进了when型程序和Until型程序分别用来处理离散行为变迁和连续模式切换，形式化地描述了混成系统的行为和性质，提出了混成建模语言的若干语义模型，我们首先以公理化的方法描述基本原子反应和组合算子的含义，探讨混成建模语言的规范型，揭示了混成系统行为的基本模式，所有不同语法形式的混成程序都可以利用代数规则转化为规范型，从而将程序行为的语义分析转化为程序规范型的语法分析，为混成系统的分析和验证提供坚实的语义基础。研究了混成系统的中断机制，构造中断程序的描述语言和语义模型，发展了混成系统中断机制的分析方法和验证技术，如：中断程序的总体执行时间、不同中断类型的中断点检查以及中断次数统计。运用提出的建模技术，对自动驾驶、车联网、多智能体等实例系统进行建模和分析，为其他类型混成系统的分析和验证提供了参考和思路。该项目共发表学术论文12篇，其中SCI论文4篇，EI论文8篇，CCF B类论文3篇，CCF C类论文4篇。