● 摘要
随着数字化设备大量的应用于装备，计算机软件在装备中的作用也越来越大，其规模呈急剧上升的趋势。软件的规模和复杂性剧增导致软件问题频出，缺陷数剧增，随着软件规模的增加其缺陷密度呈几何级数增长。软件系统规模变大以及复杂性增加，导致对系统建模的难度升高，这些问题困扰着软件工程人员。而模型分解是一种很有效的应对手段。将大模型分解成多个小模型，并依次解决这些小模型，这种办法也就成为解决以上问题的一种思路。模型分解对于规模较大的系统模型在减少缺陷、降低大规模系统复杂性、以及帮助系统可视化上会起到比较明显的效果。
Event-B语言作为一种以数学为基础的方法，能够清晰、精确、抽象、简明地描述和验证软件系统及其性质，极大地提高软件的可靠性和安全性。使用Event-B语言建立系统模型，随着系统体积的增加，模型的规模变得庞大，这时将模型分解可以有效的降低建模的难度，提高效率。本文主要研究Event-B建模过程中的各种模型分解的思路。主要研究内容如下：
1）Event-B模型分解的基本方法和思路。机器分解方法和原子分解方法是Event-B分解方法的两种基础方法。其中，机器是Event-B模型中最重要的部分，对于模型的构建和运行起着决定性的作用。对模型进行分解时不可避免的需要对机器进行分解。使用原子分解方法对模型分解，帮助精化过程的顺利进行，刻画精化过程中不同事件之间关系，可以伴随着精化过程一直使用。在机器分解方法的基础上，进一步引入了基于功能和基于结构的分解方法，拓展了Event-B模型分解的思路。
2）使用量化耦合度矩阵进行模型分解。Event-B模型中事件和变量存在耦合关系，通过分析变量事件间的耦合关联关系，分别建立变量事件耦合度矩阵、变量间耦合度矩阵、事件间耦合度矩阵，将这三个矩阵组成为表征变量事件多重耦合特性及耦合度强弱的综合耦合度矩阵，通过对综合矩阵进行聚类分析，对变量和事件分组，进而以耦合度为评判标准，将系统模型分解。
3）实例应用。对TCAS模型进行分析，应用本文提出的量化估值矩阵辅助方法，以验证方法的适用性与可行性。