1.一种基于图的邻接矩阵的形式化验证方法，其特征在于，包括下列步骤：步骤1：输入待测系统模型，进行状态编码：

步骤2：提取系统模型的状态集和原子命题集，设置原子命题集中各原子命题的编码序列，用“1”代表原子命题的逻辑“真”，用“0”代表原子命题的逻辑“假”，得到状态编码，并将状态编码的十进制值作为状态编号，用S表示状态集，s表示状态集S的状态编号集；并设置

2n×2n的方阵A，所述方阵的行、列编号与状态编号一一对应，其中n表示原子命题集的原子数目；

基于系统模型的转移关系构建有向图，其中有向图的顶点为不同的状态，有向边为状态间的转移关系；

在有向图中，若存在从状态Si到状态Sj的有向边，则将方阵A中的第i行第j列置1；否则第i行第j列置为0，得到邻接矩阵Am，其中Si,Sj∈S，i，j为状态编号；

步骤3：将用户输入的规范符号转化为规范语法树并取反后执行步骤4；

步骤4：结合邻接矩阵Am对取反后的规范语法树进行验证处理，保存满足反规范的状态，得到最终状态集：若待验证对象为逻辑算子，则直接进行逻辑计算，完成验证操作；

若待验证对象为计算树逻辑CTL算子，则继续判断待验证对象包括的CTL算子是否属于基本CTL算子集，若是，则直接进行CTL算子验证；否则对待验证对象进行CTL算子转换，用基本CTL算子集中的CTL算子进行表达后，再进行CTL算子验证；

其中基本CTL算子集包括的CTL算子为：EX、EF、EU、EG，各CTL算子的验证操作具体如下：(1)EX：

对于待验证对象EX(f)，在邻接矩阵Am中，对于任意i,j∈s，若Am[i][j]＝1，则状态Si能被EX(f)标记，其中f为CTL规范表达式；

(2)EF：

对于待验证对象EF(f)，先计算邻接矩阵Am的可达矩阵Rm；在可达矩阵Rm中，对于任意i∈s，j∈s(f)，若Rm[i][j]＝1，则Si能被EF(f)标记，其中s(f)表示包括规范符号的表达式f的状态编号集；

(3)EU

对于待验证对象E[f1Uf2]，执行下列步骤：

(3a)对于s(f1)中的每个状态编号i，s(f2)中的每个状态编号j，在邻接矩阵Am中，若Am[i][j]＝1，则将状态编号i记入集合I，其中s(f1)、s(f2)分别表示包括规范符号的表达式f1、f2的状态编号集；

(3b)剔除邻接矩阵Am中不能被f1标记的所有状态，得到子邻接矩阵Am′，并计算Am′的可达矩阵Rm′；

在可达矩阵Rm′中，对任意i∈s(f1)，k∈I，若Rm′[i][k]＝1，则Si能被E[f1Uf2]标记；

(4)EG：

对于待验证对象EG(f)，执行下列步骤：

(4a)从邻接矩阵Am中剔除所有不能被规范符号的表达式f标记的所有状态，得到子邻接矩阵Am″，将对应子邻接矩阵Am″对应的状态编号集记为s″，并计算子邻接矩阵Am″的可达矩阵Rm″，子邻接矩阵Am″的强连通矩阵SCC″，并将强连通矩阵SCC″对应的状态编号集记为scc″；

(4b)在可达矩阵Rm″中，对任意i∈s″，j∈scc″，若Rm″[i][j]＝1，则状态Si能被EG(f)标记；

步骤5：判断初始状态是否在最终状态集中，若否，则验证通过；若是，则从初始状态开始，查找一条满足反规范的路径并输出。

2.如权利要求1所述的方法，其特征在于，对任意规范符号的表达式f，所述f在系统模型的原子命题的编码序列中的位置编号用m表示，若m从1开始编号，则状态编号集s(f)的元n-m m-1 n-m m-1素的计算方式为：2 +j+k*2 ,0≤j≤2 -1,0≤k＜2 -1；若m从0开始编号，则状态编号集s(f)的元素的计算方式为：2n-m-1+j+k*2m,0≤j≤2n-m-1-1,0≤k＜2m-1，其中n为系统模型的原子命题数目。

3.如权利要求1或2所述的方法，其特征在于，步骤2还包括，对邻接矩阵Am进行精简处理：删除邻接矩阵Am中全为0的行、全为0的列，并记录精简处理前邻接矩阵Am中的非0元素对应的状态编号。