混成系统是同时包含连续状态和离散状态的动态系统。连续部分通常模拟物理环境的相互作用,而离散部分通常模拟控制系统的运行。计算和控制的结合会导致非常复杂的系统设计,因此混成系统常被应用于航空航天、汽车工业和工厂自动化设计中。到目前为止,混成系统中使用了多种形式化建模方法:混合自动机、混合Petri网、Modelica、Zelus等。对于混合系统的形式化验证,可以使用多种工具,如Hy Tech、PHAVer、d/dt、Space Ex、Flow*、Julia Reach等。这些语言和工具的共同特征是它们主要关注混合系统的高级抽象。在信息物理融合系统中,控制器被广泛设计成基于模式的周期模块,用于控制物理设备。这种系统可以在数学层面上建模为一个混成系统,即一个实时控制器程序和一个服从动态规律的交互式连续对象。嵌入式软件的设计具有相当高的复杂性,其所处的运行环境也具有不可预测的特点,这要求建模语言具有组合性和能够表达模块间的多重交互,既具有刻画嵌入式系统不同组件的能力,又能够表达环境丰富的变化情况,同时能够反应整个混成系统的模型特征。目前很多关于周期控制的语言仅仅解决了部分问题,但多数局限在只包含离散时间的离散控制系统,缺乏与所处运行环境连续行为的交互。因此,这就需要提出的语言能够对离散控制系统和连续微分动力系统进行建模,并刻画两者间的交互过程,从而实现混成系统实时感知外部的物理对象和环境变化、传输可靠性信息以及精确地控制与协调物理设备等目标,方便设计者对模型的建立、验证与分析改进。为了便于航空航天和智慧城市领域周期性混合控制系统的建模和分析,本文提出了一种面向周期控制器的层次混成建模语言（Hierarchical Hybrid Modeling Language,HHML）,该语言包含两层结构,模式抽象层和模块控制流层。前者支持在抽象层次上对混成系统进行建模,而后者用于描述模块的行为,在此框架下混成系统的控制过程和物理环境变化过程可以被统一起来进行设计和描述。此外,操作语义的引入可以帮助开发者避免自然语言的二义性来理解本语言,还可以用于形式化分析。用于形式化验证的混合自动机转换规则,为混成系统模型的设计、分析、验证和改进提供了坚实的理论基础。最后以月球着陆器为例,验证了我们所提出的方法的有效性。本文主要的贡献在于:（1）面向周期控制的嵌入式软件的混成建模语言设计:发展一种混成建模语言,使其能够形式化地统一描述嵌入式软件的控制行为和运行的物理环境。（2）混成建模语言的语义理论:研究该建模语言的操作语义,为嵌入式软件的设计、分析和验证提供语义理论基础。（3）混成建模语言的翻译规则:研究如何将HHML所建模型转换成混成自动机,从而转换到混成系统验证工具中去,使得所建模型的性质得以验证。