嵌入式系统与日常生活紧密相关，从家用电器的控制面板到航天飞行器的控制系统，无处不在。许多嵌入式系统都是安全攸关系统，任何一点错误都可能引起灾难性后果，例如核反应堆控制系统、健康医疗系统、火箭发射运行控制系统、高速列车运行控制系统等。这些系统既涉及到控制状态间的离散迁移，又涉及到物理部件的连续变化，以及离散变化和连续变化之间的交互作用。因而，传统上基于离散数学的程序设计理论已经不足以解决安全攸关复杂嵌入式系统的设计与开发的问题。如何设计安全可靠的安全攸关复杂嵌入式系统是当前计算机科学和控制论中的一个巨大挑战。特别是最近几年，随着网络的迅速发展，若干嵌入式系统通过网络连接构成信息物理融合系统(Cyber-Physical System，CPS)，使得如何高效地设计和开发安全可靠的嵌入式系统变得更加困难。　　基于模型的开发方法是嵌入式系统设计的主流方法，其基本开发流程如下:开发者首先构造待开发系统的模型，最好具有严格的形式语义;然后基于此模型进行大量的系统正确性分析和验证;最后根据此模型逐步生成系统。该方法能够在系统开发的早期有效的发现并纠正错误，从而提高开发效率与可靠性。Simulink/Stateflow是一个模型驱动的嵌入式系统建模和仿真工具，并且已经在工业界得到了广泛的使用。虽然通过对Simulink/Stateflow模型进行仿真测试可以排除一些设计错误，然而由于仿真本身的不完备性，无法仅仅依靠仿真来保证安全攸关系统的可靠性。仿真辅以形式验证技术来提高系统可靠性已经成为工业界和学术界的共识。但是，Simulink/Stateflow因为缺乏形式语义使得形式验证变得不可能。为此，本文首先使用形式化建模语言HCSP定义了Simulink/Stateflow的形式语义，并实现自动转换工具;然后，以HCSP的定理证明系统混成霍尔逻辑为基础，开发定理证明器HProver，从而提供了Simulink/Stateflow模型的形式验证框架;另外，在实际混成系统（及其对应的Simulink/Stateflow模型）中，连续物理部件的连续迁移时常带有延时，现在关于混成系统连续变化的各种验证技术均忽略这种延时。而实际中，这些延时会带来安全隐患。因此本文研究了Simulink/Stateflow中延时微分方程的渐进稳定性和安全性分析方法;最后，将文中理论成果应用于中国高速列车运行控制系统的部分重要运营场景的验证。　　本论文的主要创新性贡献包括以下几个方面。　　1.提出了将Simulink模型转换成HCSP进程的算法，并实现工具S2H。在该算法中，我们提出了Simulink模块库中除子系统以外的模块的分类方法，并分别定义了HCSP的语义模板。依据我们对Simulink模块分类，提出了Simulink模型的划分方法，实现了Simulink模型的可组合转换。该转换算法同时提供了Simulink模块的语义重写功能。　　2.提出了将Stateflow模型转换成HCSP进程的方法，并基于该算法对工具S2H进行拓展，开发了工具Sim2HCSP。提出了将Stateflow模型的转换算法与Simulink模型的转换算法进行组合的方法，从而提供了Simulink/Stateflow模型的转换方法。　　3.实现了混成霍尔逻辑的定理证明器。该定理证明器的输入为Sim2HCSP的输出，从而为Simulink/Stateflow模型提供了形式验证方法。　　4.提出了多项式延时微分方程的渐进稳定性和安全性分析方法，并实现工具iSAT-DDE。据笔者所知，目前仅有少量的方法可以分析线性延时微分方程的稳定性，而本文所述方法提出了一种针对多项式延时微分方程渐进稳定性和安全性分析的普适方法。　　5.将研究的理论成果成功应用于中国高速列车运行控制系统的验证。通过对中国高速列车运行控制系统的部分关键运营场景进行建模验证，本文确认了该系统中的一个设计错误。