随着半导体技术在过去几十年的飞速发展，片上多核处理器(MPSoC)在科学计算、无线通讯、多媒体、互联网、物联网、安全等领域得到了广泛应用，其应用渗透到人类生活的各个方面。相应地，MPSoC的设计与验证研究也成为涉及到民生关键领域的热点问题之一。大到航空航天，小到银行系统的处理芯片，不满足需求规格的功能缺陷和性能瓶颈会对人类的生命和财产安全带来危害。MPSoC是一个多任务并发系统，由于不同核处理不同任务时会相互竞争所共享的资源，核与核之间的协调是MPSoC发展非常重要的一个方面。目前针对MPSoC核协调性的验证主要集中在集成电路低层次设计（如:寄存器转换级、门级、晶体管级的电路）层面，如在系统仿真和形式化验证方面出现了大量的工具和模型，存在验证耗时、太关注实现细节，进而影响了产品面市时间等问题。本论文着眼于在MPSoC早期高层次架构设计阶段为核协调提供形式化验证的理论和方法支持，以尽早发现设计中的逻辑错误，作为MPSoC验证技术在不同层次和阶段的重要补充。　　模型检测是近三十多年来最成功的自动验证技术之一，通过显式状态搜索或隐式不动点计算来验证模型的模态/命题性质，在工业界深受推崇。本论文的研究内容涉及MPSoC核协调性早期高层次架构设计的功能性验证、安全性验证和性能验证三个方面。核心工作是采用模型检测技术，结合MPSoC的特点，对其依次进行建模、性质刻画和模型检测。涉及到混杂系统、概率时间自动机、马尔科夫决策过程、概率时序逻辑、近似等价、数值计算等相关理论的交叉和融合。此外，还对模型检测工具进行了工程领域的实现和并行化扩展。　　本论文的成果和创新性贡献主要有以下四点:　　一、将混杂系统模型和概率时间自动机模型运用于MPSoC高层次设计验证中，用离散与连续事件刻画了核间的数据交换和动态变化，以及任务调度的实时性、并发性和概率性特点。提出了一种新的用于量化数据变化的“可达比”指标，以计算在一定时间内数据变化到达目标区域的概率值。该指标作为传统的安全性、活性、公平性等属性的补充，反映了在给定调度策略下，系统到达目标功能的覆盖度。实验表明，该方法和指标在系统早期无须真正硬件实现的设计阶段，能帮助MPSoC设计者有效地对控制器策略进行功能验证。　　二、在模型检测安全性验证理论的框架下，分别对线性和非线性MPSoC数据交换进行了研究。针对线性数据交换，使用近似等价方法对状态空间进行了约简;针对非线性数据交换，通过引入保群算法，并结合欧拉方法对其优化，提出了一种新的高效数值计算方法。通过误差分析，给出了MPSoC设计安全性的定量分析，能够在给定ε误差范围内，得出系统运行是否安全的结论。　　三、通过在标记变迁系统中加入物理元器件发生故障的概率属性，构造了一种新的描述MPSoC核协调可靠性和性能的混杂马尔科夫决策过程模型。使用概率时序逻辑刻画核协调的可靠性、时间延迟和能耗等性质。最后以银行系统广泛使用的数据脱敏MPSoC为例，从稳定概率、迁移概率、权重分析、关联分析4个维度对系统可靠性和性能进行了定量分析。　　四、结合上述提出的理论体系，开发了相应的模型检测工具，并在最新的大数据平台Spark上对传统的概率模型检测工具PRISM进行了扩展，实现了矩阵乘法的并行处理。实验表明，扩展工具的求解性能在3个计算节点下性能能够提升1-2倍。