基于时间自动机的操作系统中断管理建模与验证*

王若川，杨孟飞，2，乔 磊

(1.北京控制工程研究所，北京100190;2.中国空间技术研究院，北京100094)

0 引言

操作系统在整个计算机软件体系中的重要性不言而喻.传统的测试技术难以保证此类复杂系统的设计完全正确.完全地形式化验证是已知的、并且唯一的能保证整个系统远离程序设计错误的方法［1］.

国内外学者很早就开始研究如何运用形式化的方法来验证操作系统行为的正确性.例如Walker等提出的安全内核［2］，Bevier对操作系统内核形式化模型的研究［3］，Horning等在操作系统形式化规约方面做了有益的探讨［4］.如果模型建的足够精确，确实可以很好地证明系统的可靠性.但是随着软件规模急剧膨胀，这常常是很难实现的.

通用的解决办法是优化代码结构，降低代码规模，从而降低错误出现的概率.以此为主要动机，出现了许多新概念与新技术，如安全内核与分离内核［5］、MILS 方法［6］、微内核［7］、以及隔离内核［8］等，包括CC(common criteria)［9］标准中的最高评价等级也要求待评价系统采用精简的设计.

针对一个真正的微内核，可以更好地保证其安全性和鲁棒性，从这一点上来说，有可能避免程序错误的出现［10］.澳大利亚的 Gerwin 等［1］对 SeL4微内核从顶层的抽象规约到低层的C实现，进行了完整的形式化验证，这是第一个对通用操作系统内核进行的完整的功能正确性形式化验证，确保了低层实现总是严格遵照内核行为的高层抽象规约，内核永远不会崩溃，也不会出现一些不安全的行为.

同上述关于操作系统形式化验证的研究成果相比，本文更关注动态时序正确性验证.使用时间自动机建模，使多任务能直观地在系统内执行.这是考虑到在实际工程应用中有很多严格的时间约束，从时序的角度对系统进行形式化建模与验证是很有必要的.

本文第1节简要分析某星载操作系统［11］中断管理特点，并提出验证模型;第2节给出基于时间自动机的具体建模过程;第3节结合具体例子描述如何基于以上模型进行行为正确性验证;第4节总结全文，讨论可以改进和优化的方向.

1 中断管理模型

1.1 中断管理特点

中断管理流程如图1所示，具有以下3个特点:

1)中断管理支持中断嵌套，在执行中断服务程序过程中允许更高级别的中断打断当前任务;

2)从中断服务程序返回之后首先判断是不是最外层中断，结果为假则进行中断上下文恢复，继而返回到更外一层的中断程序中去.结果为真则进行中断级的任务调度;

3)中断级的任务调度主要进行两个判断:就绪态任务的最高优先级是否大于当前运行任务的优先级，当前运行任务的时间片是否已经用完.若有任意一个判断结果为真，则进行任务的上下文切换.若两个判断结果都为假，则进行正常的中断上下文恢复.

1.2 对象实体

由图1可以看出，中断管理与一组硬件设备相关，本文将它们抽象为4类对象实体，分别是:CPU、中断控制器、中断请求源和存储设备.

1.3 服务行为

上文已经抽象出了中断管理模块涉及的对象实体，侧重描述了该模块的静态属性.下面将中断管理的动态属性抽象为4个服务行为，它们分别是:中断上下文保护行为、执行中断服务程序行为、中断级任务调度行为、中断上下文恢复行为.

图1 中断管理流程图Fig.1 Flow diagram of interrupt management

值得注意的是，所有的对象实体都是独立于中断管理的服务而存在的，中断管理服务的能力体现在与对象实体的交互，使对象实体的状态发生改变.一种中断管理服务总是与特定的对象实体集交互完成的.

1.4 中断管理验证模型

基于以上的分析，进一步提出中断管理验证模型，如图2所示.

图2 中断管理验证模型Fig.2 Verification model of interrupt management

2 基于时间自动机的建模过程

2.1 时间自动机

由Alur和Dill所提出的时间自动机［12］是一种对实时系统行为建模的工具，它是一种简单的、却强有力的描述方式.定义为一个有穷定向图，由一组可被重置的非负实值时钟和时间约束所标注.特定的时间自动机接收特定的时间字.下面给出本文使用的时间自动机定义.

定义1.一个时间自动机(TA，timed automata)是一个六元组(L，l0，C，A，E，I)，其中 L是位置的集合，l0∈L是初始位置，C是时钟变量集，A是动作集，包括自动机内部动作及自动机间动作，E⊆L×A×Φ(C)×2C×L是边集，由位置、动作、保卫公式、需要被重置的时钟变量集所组成，I:L→Φ(C)，将一个位置映射为一个保卫公式，称为状态的不变量(invariant).

定义2.假设有n个时间自动机TA1，…，TAn，其中给定任意自然数i，对 1≤i≤n，TAi=(Li，li0，Ci，Ai，Ei，Ii)，由这n个时间自动机构成的网络记为N=TA1||TA2|| … ||TAn.格局(configuration)是用来描述网络中所有自动机运行时的状态(全局状态)的概念.

2.2 对象实体建模

对象实体的形式化描述如下:

定义3.一个对象实体类为T=＜Tid，A，O，M＞，其中Tid为对象实体类的标识符;A为对象实体属性的集合;O为对象实体操作的集合;M表示从属性集合到各个数据类型的一个映射，数据类型包括基本数据类型如Int、Boolean、Float等，也包括用户自己定义的类型.将所有对象实体类的集合记为TOE，对于任意的T∈TOE，T.A表示类型T的所有属性，T.O表示类型T的所有动作.

在对象实体类的基础上，可以创建具体的对象实体.

定义4.一个对象实体为三元组t=＜tid，T，TA＞，其中tid为该对象实体唯一标识符;T∈TOE表示该对象实体所属的对象实体类;TA=(L，l0，C，A，E，I)为符合定义1的时间自动机，用于描述环境实体的动态行为.

根据上述定义所得到的对象实体和对象实体类就构成了中断管理验证模型中的对象实体库.采用时间自动机，一个属于存储设备类的对象实体可表示为如图3所示.

图3 存储设备时间自动机描述Fig.3 Timed automata of memory

2.3 服务行为建模

服务行为的形式化描述如下:

定义5.一个服务行为可形式化地表示为一个三元组＜Sid，Eset，STA＞，其中Sid为该行为的唯一标识符;Eset⊆TOE表示与该行为有交互的对象实体类的集合;STA为一个时间自动机，用于描述行为的动态特征.

例如，中断上下文保护行为可表示为＜IProtect，{EMemory，EInterruptController}，SIP＞，其中SIP如图4所示.

图4 中断上下文保护行为时间自动机描述Fig.4 Timed automata of context protection behavior

2.4 环境建模

定义6.假设一个 OS行为S= ＜Sid，Eset，STA＞，环境实体集合Env=∪n i=1＜i，Ti，ETAi＞ 称为S的一个环境，若满足对于任意T∈Eset，存在1≤i≤n使Ti=T，即对于服务中的每个对象实体类，在环境中都至少存在该类的一个实例化对象实体.行为S与它的环境Env之间的交互用时间自动机网络STA||ETA1||…||ETAn来表示.

到目前为止，OS行为与它对应的运行环境已经完全建模为时间自动机网络，对行为的正确性验证实际上转化成了对相应时间自动机网络的分析.

3 中断管理验证

下面以一个具体的行为以及与该行为相关的两个实体为例来说明验证过程，将中断管理模块行为的时序正确性分解为以下3类性质:

1)可达性(reachability)，即考察是否存在一条从初始状态开始的路径，沿着这条路径最终φ被满足.在Uppaal中书写该条性质的语法为E＜＞φ.

2)安全性(safety)，即不好的事情永远不会发生.在Uppaal中记为A［］φ，A表示在所有可达的状态中φ都是真的.例如在任何情况下，都不希望操作系统发生死锁.

3)活性(liveness)，即某件事最终是会发生的.常用的一种形式是“导致”或者“反应”，记为φ→Φ，意思是任何时候只要φ被满足，那么最终Φ将会被满足.在Uppaal记作φ→Φ.例如一个中断产生以后，最终是会被响应的，而不会被无限期地搁置.下面是具体的例子.

中断上下文保护行为发生在新中断到来的时候，它与存储设备和中断控制器两个实体相交互.存储设备和上下文保护行为的自动机分别见图3和图4，图5是中断控制器的自动机模型.

中断控制器的时间自动机带有一个形式参数，用来表示该自动机描述的中断等级，这里假设一共有三级中断，第三级的优先级最高.

对中断管理的正确性验证需要将行为和相关的环境组合成一个整体系统:

首先要验证的性质是在任何情况下，都不希望系统出现死锁，验证输入逻辑公式为:A［］not deadlock，验证通过.

图5 中断控制器时间自动机描述Fig.5 Timed automata of interrupt controller

其次验证系统一些比较重要的状态可达性.这里举其中一例说明，输入公式为:E＜＞InterruptProtect.Can_not_be_interrupted，表示关中断以后的状态是可以达到的，验证通过.其余可达性同理均验证通过.

再次是安全性验证，输入公式为:A［］Interrupt-Controller1.S2+InterruptController2.S2+Interrupt-Controller3.S2＜=1，意思是任何情况下只能保存一个中断的现场，不可能出现关中断后有两个或以上中断需要被保存的情况，验证通过.

最后验证活性，输入公式为:Curlevel==3--＞ not InterruptController1.S2 Curlevel==3-- ＞not InterruptController2.S2表示的意思是如果当前是第三级中断抢占了CPU资源，那么低级中断无法打断高级中断的执行，验证通过.

部分性质的验证结果如图6所示.同理可以验证中断管理其他行为的时序正确性，从而说明，该模块满足设计需求.

由于涉及到多个时间自动机的联动，使状态空间爆炸问题更加突出.下一步工作的重点是使用偏序技术［13-14］来约简时间自动机的状态空间，使其能尽可能的精简，从而提高正确性验证的效率.

图6 性质验证结果Fig.6 Verification results

4 结论

本文在分析某嵌入式操作系统中断管理模块的基础上，着眼于时序特性，提出了一套形式化建模与验证方法:提取出不同的对象实体和系统行为，并且运用时间自动机理论对它们分别建模，将它们之间的相互作用关系转化为时间自动机网络的描述.同时将需要验证的一系列时序性质使用形式化方法表示，并输入到该时间自动机网络中，利用模型检测工具箱Uppaal验证了这些性质，证明了其服务行为的正确性.

［1］GERWIN K，JUNE A，KEVIN E，et al.SeL4:formal verification of an OS kernel［J］.Communications of the ACM，2010，53(6):107-115.

［2］WALKER B，KEMMERER R，POPEK L.Specification and verification of the UCLA unix security kernel［J］.Communications of the ACM，1980，23(2):18-131.

［3］BEVIER W.A verified operating system kernel［D］.Austin:University of Texas，1987.

［4］BIRRELL A，GUTTAG J，HORNING J，et al.Synchronization primitives for a multiprocessor:a formal specification［R］.New York:Gilles，1987.

［5］U.S.Government protection profile for separation kernels in environments requiring high robustness［R］.Washington D.C.:Information Assurance Directorate，2007.

［6］ALVES J，OMAN P，TAYLOR C，et al.The MILS architecture for high-assurance embedded systems［J］.International Journal of Embedded Systems，2006(2):239-247.

［7］HOHMUTH M，PETER M，H¨ARTIG H，et al.Reducing TCB size by using untrusted components—small kernels versus virtual-machine monitors［C］∥Proceedings of the 11thACM SIGOPS European Workshop.Belgium:Leuven，2004:53-79.

［8］WHITAKER A，GRIBBLE S.Scale and performance in the Denali isolation kernel［C］∥Proceedings of the 5thSymposium on Operating Systems Design and Implementation.Boston:Godefroid，2002:195-210.

［9］The National Security Agency.ISO/IEC 15408 common criteria for information technology security evaluation［S］.Gaithersburg:the National Institute of Standards and Technology(NIST)，2009:32-38.

［10］ELPHINSTONE K，KLEIN G，DERRIN P，et al.Towards a practical，verified kernel［J］.International 11thWorkshop on Hot Topics in Operating Systems，2007，75(3):117-122.

［11］QIAO L，GU B，YANG H，et al.An embedded operating system design for the lunar exploration rover CPS［J］.The First International Workshop on Safety and Security in Cyber-Physic-al Systems，2011(6):88-101.

［12］ALUR R，DILL D.A theory of timed automata［J］.Theoretical Computer Science，1994，126:183-235.

［13］BENGTSSON J，JONSSON B，LILIUS J.Partial order reductions for timed systems［C］∥Proceedings of the 9thInternational Conference on Concurrency Theory(CONCUR98).Netherlands:Zindhoven，1998:485-500.

［14］MINES M.Partial order reduction for modeling checking of timed automata［C］∥Proceedings of the 10thInternational Conference on Concurrency Theory(CONCUR99).Netherlands:Zindhoven，1999:431-446.