随着计算机软件和硬件技术的进步,软硬件系统的性能有了很大程度的提升,系统变得越来越复杂的同时,也更容易出现差错。与传统的仿真和测试技术相比,形式化方法基于严格的数学理论,能够准确地对系统进行描述和建模,并可以用模型检测技术对系统需要满足的性质进行验证,具有高可信度和自动化的特点。因此,形式化方法已经被大量运用于软硬件系统设计与开发中。然而,随着系统覆盖面积的提升,软件和硬件的规模不断扩大,系统呈现出高并发的特点,模型检测过程中经常会出现状态空间爆炸的问题。本文在研究现有的组合方法和抽象方法后,对这两种方法进行了调整与结合,并引入层次化的思想,给出了基于层次组合抽象的建模与验证方法。该方法可以根据系统的特点来进行分层建模,旨在及时发现系统设计中的缺陷,同时通过减少系统冗余状态,来缓解检测中状态空间爆炸的问题。本文主要工作如下:(1)对经典的组合和抽象方法的规则进行了扩展,给出适用于复杂系统形式化建模与验证的方法:引入层次化建模思想,根据特点将系统划分为多层次进行建模,并用Kripke结构描述系统层次模型,通过定义层次模型之间的组合规则以及层次组合模型的抽象规则,将各层的Kripke结构模型进行组合抽象处理,得到系统的层次组合抽象模型,接着将Kripke结构转化为CSP#(Communication Sequential Process Sharp)模型,并制定了相应的验证策略。(2)以能源共享系统为例,对能源共享系统的组成结构进行了分析与建模,用形式化的方式对系统的层次结构进行定义,便于对系统各层之间的输入输出关系进行分析,为系统模型的建立以及形式化规约奠定理论基础。(3)利用形式化语言CSP#对系统模型进行形式化规约,采用线性时序逻辑LTL(Linear Temporal Logic)描述系统需要满足的性质,使用PAT(Process Analysis Toolkit)工具对系统模型进行自动化检测,找出系统设计缺陷并加以改进。实验结果表明,该方法能够在找出能源共享系统中的设计缺陷的同时,有效缓解模型检测中的状态空间爆炸问题。