时间自动机模型的安全计算机平台的形式化验证分析.docVIP

时间自动机模型的安全计算机平台的形式化验证分析 　　摘要：越来越多的工业领域对计算机控制系统的可用性、可靠性和安全性要求越来越严格，而2乘2取2冗余结的计算机平台正是解决这一问题的一种重要方式。本文通过分析CBTC系统安全计算机平台各组成结构的基础上，提取出了时间自动机的校验助手UPPAAL，并通过建立一个系统模型，在此基础上再进行验证和分析。 　　关键词：计算机；时间自动机；模型验证 　　中图分类号：TP301.1 文献标识码：A 文章编号：1674-7712 （2012） 18-0049-01 　　一、时间自动机和它的验证助手UPPAAL 　　Alur创立了时间自动机，它被称为一种计算模型，能够充分地描述系统的行为。一个一个的时间自动机TA1，…，TA通过并行的复合就构成了时间自动机的网络，每个TAi（1≤i≤n）称为时间自动机的每一个进程，所有这些进程的通信是通过通道或共享全局变量的方式而实现的，同步通信的实现是以运用输入和输出动作而获得握手同步的方式，异步通信的实现是以共享全局变量的方式。要想真正实现模拟握手同步这一目标，时间自动机在标记中主要含有两个动作符号，即输入的符号a？和输出的符号a！。 　　时间自动机的验证助手UPPAAL是一个为集成的实时系统提供建模和验证环境情况的助手，可以在此适用叙述成不确定的并行过程的积的系统。每一个过程都可以理解为由实数值时钟、变量和有限控制的结构而构成的时间自动机，过程之间通信的实现是利用管道和共享的变量而实施的，管道的最大益处是可以使不同的自动机中的两个转换能够一块进行。在建立一个比较完整的性质自动机和系统自动机后，才可以对自动机理论的模型检验方法进行验证，UPPAAL采用了一种称为“on-the-fly”的搜索技巧，在跟性质自动机的乘积相判空的情况下，如果有需要，系统自动机的状态就可以生成了，如此是不需要为系统建立全部的状态空间，这样就使模型验证器的效率得以提高。 　　二、时间自动机的系统建模 　　（一）系统的结构和功能。由容错安全管理（FTSM）单元和6台工控机组成了安全计算机平台的系统，它一共分成了3个模块，如图1所示。 　　每个模块的组成和功能有： 　　1.处理单元模块：2乘2取2的结构是由4台工控机组成的，4台工控机各自叫做处理单元的PUA1、PUA2、PUB1、PUB2，其中，2取2结构的通道A是由PUA1与PUA2、PUB1与PUB2组成的，通道B的作用是在处理的结果输出至数据输入输出模块之前，处理输入数据。 　　2.数据输入输出的模块：它是由两台工控机构成的负责输入输出数据转发的。 　　3.安全表决模块：它是由两个容错的安全管理单元FTSMA和FTSMB组成，可以实时检测数据输入输出的模块和处理单元的模块的6台工控机。表决通道A、B的主备状态的切换可以在此进行，还可以对通信控制器的状态进行控制。 　　4.2取2的通道之间的切换：这两个通道的状态模式主要有断电模式、状态模式、跟随模式、上电模式、备通道模式和主通道模式。 　　（二）通道内2取2双机的同时进行。在通道内2取2双机的工作流程之间的同时进行关系不是很宽松的。一定要在第三方的FTSM单元进行判决后，才能够实行2取2双机的同时进行，一定要在相同的时间间隔内确保FTSM的单元部分收到双机的同时进行的提示，同时进行被判定成功后，及时告知要求同时进行的双方获取同时进行的成功；如果ISM的单元部分在同时进行的时间间隔之内没有获得相应的同时进行的要求，就能认为双机的同时进行是失败的。电的初始同时进行的时间范围要求在480个单位之内，处理单元时的操作周期却是340个单位，一共可以分成4个微周期，即正常的同时进行的周期，输入数据的周期，ZC应用的周期和输出数据的周期，同时进行的时间各自为20、60、200、60个时间单位。在处理的单元部分上，如果存在一步的FTSM认定为双机不能够同时进行，这是就要重新开启处理的单元PU1，PU2，于此同时，FTSM也就进入了一个初始的状态。 　　三、验证过程分析 　　在验证的时候，就会出现一些在设计上不够合理的位置。比如，FTSM规定在通道内的双机的同时进行的时间间隔是各微周期的时间长度，也就是说双机同时进行的时差最大的值是每个微周期的时间长度，这种现象是不合乎逻辑的。用输入数据的微周期为一个例子，它的验证 　　语句是： 　　双机的同时进行的时间限制是每个微周期的时间长度： 　　A[]（ftsmA.DatalnDoneimPly（timerAI一timerAZ）=60 and（timerAI- 　　timerAZ）=一60）. 　　双机同时进行的时间差的最大值是每个微周期的时间长度： 　　E（ftSInA.DatalnDoneand（timerAI一