综合模块化航空电子系统已被广泛应用于航空、航天等安全关键领域,其主要目标是实现分区操作系统,为多个安全级别的子系统提供资源共享的运行平台,并采用时间隔离和空间隔离机制保证应用程序之间的故障隔离和信息流控制。由于分区操作系统的复杂性,其安全性和可靠性往往难以通过测试和仿真手段来保证。需要采用严格的形式化方法,建立清晰的、无二义的数学模型,并采用数学推理和验证的手段来保证其时间隔离能力和空间隔离能力。当前对分区操作系统的建模及验证工作主要包括采用定理证明方法来验证其空间隔离属性或采用模型检测方法来验证其时间隔离属性,缺乏一个统一的框架来完整地解决时间和空间隔离属性的形式化建模及验证工作。这主要是由于定理证明类的建模语言通常无法建模系统的控制流和时间,也无法表达并发对象的交互行为。反之,模型检测方法所使用的工具和语言通常都缺乏良好的逐步精化框架,对数据密集型的系统的建模和验证能力也存在不足。本文以分区操作系统的建模及验证需求为牵引,针对定理证明类建模语言Event-B和模型检测方法LTS以及时间自动机的缺点,提出了一种组合形式化方法,给出了一个基于组合形式化方法的分区操作系统建模及验证框架,构建了Event-B的行为语义模型和时间语义模型。在此基础上,完成了分区操作系统的行为属性和时间属性的建模及验证。所完成的工作和创新点主要体现在以下几个方面:（1）研究了Event-B建模语言和模型检测类的形式化建模语言的组合建模问题,提出了一个基于组合形式化方法的分区操作系统建模及验证框架。本文针对Event-B和LTS、时间自动机等方法的局限,提出了一种“相互表示”的方法,用Event-B状态机来表示LTS和时间自动机的建模元素。在此基础上,提出了一个组合Event-B和LTS以及时间自动机的系统建模及验证框架,为组合使用多种形式化方法完成复杂系统建模及验证提供了一种新的思路。（2）研究了Event-B建模语言的行为语义模型和时间语义模型,并完成了这些语义模型的正确性证明。本文针对Event-B建模语言缺乏行为语义和时间语义的局限,使用LTS表达Event-B的行为语义,并使用时间自动机表示Event-B的时间语义;给出了从Event-B模型到LTS模型及时间自动机模型的转换规则,并采用LTS之间的互模拟等价关系证明了Event-B模型和其对应的行为语义模型及时间语义模型的行为等价性,为组合使用Event-B建模语言和LTS及时间自动机完成分区操作系统建模和验证奠定了理论基础。（3）研究了LTS和时间自动机等模型检测类建模语言的逐步精化方法,并给出了一个逐步精化框架。传统的模型检测类建模语言通常都缺乏从抽象模型到具体模型的逐步精化框架,给系统建模和分析工作带来很大的困难。本文针对这一弊端,借鉴了Event-B的逐步精化过程,提出了LTS和时间自动机模型的逐步精化框架,将模型的演化过程归纳为在垂直方向上对某个对象的行为的分解以及在水平方向上逐步引入更多的并发对象,并给出了各种垂直精化模式和水平扩展模式,为开发多视图的组合形式化模型提供了新的思路。（4）在上述工作的基础上,构建了分区操作系统的行为模型及时间模型,完成了分区操作系统的行为属性验证和可调度性验证。在前述工作的基础上,本文首先使用定理证明语言Event-B构建了分区操作系统规范ARINC 653的模型,并将其转换为等价的LTS模型,通过验证LTS模型的行为属性保证了Event-B模型的相应属性。而后,使用Event-B搭建了分区操作系统的两级调度模型,并将其转换为对应的时间自动机模型;通过验证时间自动机模型的可调度性保证了Event-B模型的可调度性。通过以上两个模型的构建和验证,证明了本文所提出的组合形式化方法的实用性。