基于Event-B的中断管理需求和设计形式化建模与验证方法*

周育逵,杨 桦,乔 磊

(北京控制工程研究所,北京 100190)



基于Event-B的中断管理需求和设计形式化建模与验证方法*

周育逵,杨 桦,乔 磊

(北京控制工程研究所,北京 100190)

随着软件复杂度的迅速增长，传统的基于测试的方法逐渐难以满足航天器操作系统的可靠性和安全性需求，形式化方法逐渐成为航天器操作系统安全可靠性的有效保障.基于Rodin平台，采用Event-B形式化语言，通过需求和设计重写、制定精化策略并逐步精化的方法，对航天嵌入式操作系统SpaceOS2的中断管理模块建立了需求层和设计层形式化模型，将模型检验和定理证明相结合，验证模型的正确性并且满足安全性质. 关键词： 中断管理;形式化验证;Event-B;精化

0 引 言

在航空航天领域，航天器操作系统的安全性因其生命期长，结构复杂，稳定性要求高和出错代价高昂开始引起了广泛的关注.操作系统由于其复杂性，其正确性很难用定量的方式进行描述和说明，由于操作系统软件在各类航天器计算机应用中的核心地位，其可靠性至关重要.随着软件复杂度的迅速增长，传统的基于测试的方法逐渐难以满足航天器操作系统的可靠性和安全性需求，形式化方法逐渐成为航天器操作系统安全可靠性的有效保障，采用形式化的方法对操作系统进行设计和验证[1-2]已经得到国际学术界的广泛重视.

形式化方法[3]是建立在严格数学基础上的用以对软硬件系统进行说明、设计和验证的语言、技术和工具的总称，分为形式化规约与形式化验证两个方面.形式化规约就是用形式化语言在不同抽象层次上描述系统的行为与性质.形式化验证是基于已经建立的形式化规约，对软件的相关特性进行评价的数学分析和证明.形式化验证主要包括模型检验[4]和定理证明[5]两个方面，模型检验主要是利用对系统问题建立的数学模型进行自动推理.定理证明一般采用交互式的定理辅助证明器来对系统问题进行抽象描述，并以数学公式定理的方式表达系统的功能和性质，采用数学定理推导演算的方法进行验证.

操作系统形式化验证工作可以追溯到20世纪70年代，美国加利福尼亚大学洛杉矶分校的Secure Unix项目[6]就对Unix的安全内核进行了形式化描述与验证工作，其研究重点在于内核规范.美国德克萨斯州大学的Bevier建立了内核形式化模型[7]，Horning[8]对操作系统的规约进行了形式化描述，Zhou和Black[9]运用HOL定理证明器对操作系统安全行为操作的形式化描述进行了研究.

近年来，国外针对操作系统的验证还有：德国德累斯顿工业大学的VFiasco项目[10]、美国霍普金斯大学的EROS/Coyotos项目[11]、德国的Verisoft项目[12]与后续的Verisoft-XT项目[13]、澳大利亚国家通讯技术研究中心的L4.Verified项目[1,14]等.其中，澳大利亚的L4.Verified项目组[1]在2009年宣布成功验证了一个可以实际应用的操作系统内核seL4，并宣布它是第一个针对功能正确性结果完全的形式化验证的通用操作系统内核.

国内研究机构从20世纪90年代开始进行大量的工作，近年来也取得了重要成果，比如中国科学技术大学的μC/OS-Ⅱ验证项目设计了并发精化验证框架并在Coq中实现了该理论框架[15]，其目标是完成嵌入式并发多任务操作系统μC/OS-Ⅱ的数学验证；南京大学钱振江博士研究了安全操作系统的形式化设计与验证方法[16]，提出了操作系统对象语义模型，并给出如何验证操作系统在运行过程中保持安全策略和属性的形式化描述方法等.

本文基于Rodin[17]平台，采用Event-B[18]形式化语言，通过需求和设计重写、制定精化策略并逐步精化的方法，对航天嵌入式操作系统SpaceOS2的中断管理模块的需求和设计进行形式化建模，将模型检验和定理证明相结合，对模型和安全性质进行了验证.

1 需求重写和设计重写

Abrial[18]提到的形式化开发方法中指出，为了建立正确的系统，首先需要谨慎地编写需求文档，进行需求重写，其原因是企业通用的需求文档往往晦涩难懂，不适合形式化建模.

本文将需求重写延伸至设计层，把需求重写和设计重写作为形式化验证的第一步.将原始的需求和设计按照以下3类进行重新分类整理：

FUN：功能，用于描述系统主要功能，软件需要完成的具体任务.

ENV：环境，考虑系统或软件所处环境，包括与其相关的设备、物理现象、其它软件/系统/模块以及用户.

SAF：安全性质，指的是系统需要满足的一些性质，它们能保证系统或软件正常运行，不发生错误，不发生典型的缺陷.

然后对重新整理后的需求项和设计项进行标号，建立精化策略，通过制定精化策略在精化模型中引入需求项和设计项并逐步精化，直到完成形式化建模与验证.

2 需求层建模与验证

2.1 需求重写

对需求规格说明书中的中断管理模块的需求进行重写，按照功能、环境和安全性质进行分类标号，标号以R(Requirement)开头，并建立中断管理模块的原始需求规格说明和重写后的需求的对应关系便于追溯.

中断管理模块通过中断管理程序实现，对中断管理模块相应的需求进行重写后共形成功能需求3条，环境需求2条，安全性质1条，如表1所示，并建立原始文档中的需求和重写后需求项的对应关系，来说明重写后的需求能覆盖原始文档中的需求.

2.2 需求层精化策略

需求层对中断管理程序的3个主要功能建立抽象模型，对外部环境建立抽象模型，并建立中断管理和外部环境之间的交互关系.

需求层分两层进行精化，在L0-R0层引入功能和环境需求，在L0-R1层引入安全性质.精化策略表如表2所示.

表1 功能需求、环境需求和安全性质Tab.1 Requirements of function、environment and safety

表2 需求层精化策略Tab.2 Refinement strategy table of requirement model

注.*表示该项在该层没有被完全引入

2.3 需求层模型

根据需求重写项和需求层精化策略在Event-B内建立需求层模型，需求层模型分为L0-R0和L0-R1共2层，由1个场景(Context)和2个机器(Machine)组成，如图1(a)所示，其中macL0R1是对macL0R0的精化，需求层模型中的机器和场景间的关系如图1(b)所示.

场景ctx0中使用集合、常量和公理定义了模型的静态元素，机器macL0R0和macL0R1分别对应需求层的L0-R0层和L0-R1层，机器定义了模型的动态行为，包括系统变量(Variables)、不变式(Invariants)、事件(Events).不变式是一个正确性断言，它断言了程序或模型中变量之间的某些联系，当变量的状态发生改变时要求改变之后的变量仍然满足该约束条件，上下文保护和恢复、执行ISR等操作通过事件进行建模.

L0-R0层模型中建立了场景ctx0和机器macL0R0，描述中断管理的3个基本步骤：上下文保护、执行ISR和上下文恢复，引入和中断处理程序进行交互的外部环境：中断源、中断控制器和IU单元.

在macL0R0中定义了10个事件：设置模型状态(SetState)、设置起点(SetBegin)、设置起点状态具体值(BeginWith)、中断源(IntSrc)、中断控制器(IntCtrl)、IU单元(IUnit)、上下文保护(CtxSave)、执行ISR(RunISR)、上下文恢复(CtxRecov)、中断返回(Return).事件举例：事件CtxRecov对上下文恢复进行建模，当状态为ctxRecov时进行上下文恢复，该条件由卫兵grd1进行约束，需求层模型中使用布尔赋值将上下文恢复的操作抽象成act1，在设计层精化中进行进一步精化，CtxRecov的定义如下：

WHEN

grd1: state = ctxRecov

THEN

act1: ctxrecov :∈ BOOL

END

L0-R1层模型中引用了场景ctx0，建立了机器macL0R1，进行的主要操作是对事件间的交互关系进行精化和规约，从而保证需求层能够满足安全性质.

关于需求层的安全性质，安全性质R-SAF-1描述了中断管理程序的3个步骤之间的顺序关系，要保证上下文保护、执行ISR、上行文恢复顺序执行，根据已经建立的模型，给定状态下只有对应该状态的事件能够执行，即只有在状态ctxSave时才能进行上行文保护，只有在状态runISR时才能执行ISR，只有在状态ctxRecov时才能进行上行文恢复，然后由事件TopSequenceCtrl控制状态转换，因此该安全性质通过在事件TopSequenceCtrl中加入以下卫兵进行规约：

grd_save_isr: state = ctxSave ⟹ next_state = runISR

grd_isr_recov: state = runISR ⟹ next_state = ctxRecov

grd_recov_rtn: state = ctxRecov ⟹ next_state = return

精化完成后，需求层模型结构如图2所示.

2.4 需求层验证

在需求层建模过程中会生成证明义务(Proof Obligations, PO)，包括建立安全性质时也会生成相应的证明义务，需求层模型的正确性和安全性由以下两点确保:一是证明义务能够被证明，二是模型不存在死锁和不变式违反案例.

需求层模型中生成的证明义务都能够被自动证明，统计结果如图3所示.

使用ProB[19]对macL0R1进行模型检验，没有死锁和不变式违反情形，即deadlocked、invariant_violated和invariant_not_checked的计数都为0，结果如图4所示.

以上验证结果验证了中断管理需求层模型的正确性和一致性.中断管理需求层原始文档中自然语言需求有15个，对应需求重写后的功能需求3个、环境需求2个、安全性质1个，通过形式化描述，这些需求和性质都被引入到形式化模型中，并生成了21条证明义务，通过工具验证，模型中所有的证明义务都得到了证明，并且没有发现死锁和不变式违反案例，从而证明了模型的正确性和安全性.

3 设计层建模与验证

3.1 设计重写

对详细设计中的中断管理程序的设计说明进行重写，按照功能、环境和安全性质进行分类标号，标号以D(Design)开头.对中断管理程序的设计说明中的流程图的每个处理步骤进行编号，然后与设计重写后的项目建立对应关系，来说明重写后的设计项能覆盖原始设计项，并建立设计重写后的项目与需求重写后的项目的对应关系，来说明两者的一致性.

设计重写后共形成功能项12条，环境项4条，安全性质6条，部分举例如表3所示.

表3 设计层功能、环境和安全性质举例Tab.3 Part of functions、environments and safeties of design model

3.2 设计层精化策略

设计层共分4层对需求层建立的抽象模型以及交互关系进行精化.

L1-D0层：L1-D0层对中断管理的3个步骤上下文保护和恢复、执行ISR进行精化.一些必须但复杂的功能在后续精化层中引入，比如在L1-D0层不引入上下文保护的判断条件，在后续的精化过程中引入判断条件后再根据判断条件将上下文保护精化成多个事件.

此外，对外部环境进行适当精化，中断源进行中断请求，中断控制器进行筛选判优，IU单元响应中断、设置PC值，中断返回恢复PC值，对初始化操作进行精化.

L1-D1层：引入中断嵌套、开/关中断，并根据嵌套数、被中断的程序类型(是否为任务)对上下文保护和恢复进行分类.

引入一个事件对嵌套数计数.引入中断屏蔽，并据此加强中断响应的卫兵条件(必须是开中断并且未被屏蔽)等.考虑上下文保护和恢复的精化：引入两个事件对上下文保护进行精化，引入两个事件对上下文恢复进行精化，引入两个事件分别对任务重调度和任务切换进行建模.

引入了开关中断，因此在IU单元的操作中加入关中断操作，中断返回操作中加入开中断操作.

L1-D2层：引入窗口上下溢标志并根据标志对窗口上下溢的处理，用两个事件分别对窗口上溢和下溢进行建模.

IU单元和中断返回中涉及窗口的操作，进行相应的精化.

L1-D3层：引入各个事件间的执行顺序等关系，描述安全性质.

设计层精化策略表如表4所示.

表4 设计层精化策略Tab.4 Refinement strategy table of design model

注：*表示该项在该层没有被完全引入

3.3 设计层模型

根据设计重写项和设计层精化策略在Event-B内建立设计层模型，设计层模型分为L1-D0、L1-D1、L1-D2和L1-D3共4层，建立3个场景ctx1、ctx2和ctx3，依次对ctx0、ctx1、ctx2进行扩展(Extend)，建立4个机器macL1D0、macL1D1、macL1D2和macL1D3，依次对macL0R1、macL1D0、macL1D1和macL1D2进行精化，如图5(a)所示，设计层模型中的机器和场景间的关系如图5(b)所示.

模型精化举例：L1-D1层引入中断嵌套后，事件CtxRecov1和TaskReschedule共同精化抽象事件CtxRecov，当满足卫兵条件IntNestCnt > 1 ∨ TaskCur = 0时，由CtxRecov1进行有嵌套(嵌套数>1)或当前任务为0(被中断的程序不是任务)时的上下文恢复，当满足卫兵条件IntNestCnt = 1 ∧ TaskCur ≠ 0时，无嵌套(嵌套数=1)且当前任务非0(被中断的程序是任务)，需要调用任务重调度函数，由TaskReschedule进行处理，在TaskReschedule中对need_task_switch进行赋值，标志后续是否需要任务切换.TaskReschedule的定义如下：

REFINES

CtxRecov

WHEN

grd1: state = ctxRecov ∧ setTopSeq = TRUE

grd2: IntNestCnt = 1 ∧ TaskCur ≠ 0

THEN

act1: ctxrecov := TRUE

act2: setTopSeq := FALSE

act3: need_task_switch :∈ BOOL

END

事件CtxRecov1和TaskReschedule共同规约了功能项D-FUN-9.

下面描述如何对子步骤间的交互关系进行精化.以上下文保护为例，由事件SetSaveSequence来控制上下文保护中的各个子步骤间的状态转换，上下文保护一共分为5个子步骤，5个子步骤间是顺序执行关系，通过以下卫兵条件进行规约：

grd_save_0_1: save_state = save_s0 ⟹ next_save_state = save_s1

grd_save_1_2: save_state = save_s1 ⟹ next_save_state = save_s2

grd_save_2_3: save_state = save_s2 ⟹ next_save_state = save_s3

grd_save_3_4: save_state = save_s3 ⟹ next_save_state = save_s4

执行ISR的子步骤间的交互关系由事件SetIsrSequence控制，上下文恢复的子步骤间的交互关系由事件SetRecovSequence和SetSchedSequence共同控制，规约和精化方法与上文描述的方法一致，不再赘述.

子步骤间交互关系的精化主要体现在上下文保护、执行ISR和上下文恢复中，IU单元处理完成后进入上下文保护，当处于上下文保护步骤中时(inSave = TRUE)，由SetSaveSequence控制上下文保护中的各个子步骤间的执行顺序，当跳出上下文保护步骤时(┑(inSave = TRUE))，由TopSequenceCtrl控制进入下一步骤即执行ISR；当处于执行ISR步骤中时(inIsr = TRUE)，由SetIsrSequence控制执行ISR中的各个子步骤间的执行顺序，当跳出执行ISR步骤时(┑(inIsr = TRUE))，由TopSequenceCtrl控制进入下一步骤即上下文恢复；当处于上下文恢复步骤中时(inRecov = TRUE)，由SetRecovSequence控制上下文恢复中的各个子步骤间的执行顺序，当跳出上下文恢复步骤时(┑(inRecov = TRUE))，由TopSequenceCtrl控制进入下一步骤即中断返回.

下面介绍安全性质.在L1-D3层模型中对设计层的安全性质进行规约，比如D-SAF-5对应不变式inv_DSAF5_1和inv_DSAF5_2，其中inv_DSAF5_1的含义是关中断时不能进行中断响应，具体内容如表5所示.

表5 设计层安全性质的规约Tab.5 Specifications for safeties of design model

精化完成后，设计层模型结构如图6所示.

3.4 设计层验证

在设计层建模过程中会生成证明义务，包括建立安全性质时也会生成相应的证明义务，设计层模型中生成的证明义务都能够被证明，统计结果如图7 所示.

使用ProB对macL1D3进行模型检验，没有死锁和不变式违反情形，即deadlocked、invariant_violated和invariant_not_checked的计数都为0，结果如图8所示.

以上验证结果验证了中断管理设计层的正确性和一致性.中断管理设计层原始文档中的项目有50个，对应设计重写后的功能项12个，并针对设计层列出环境项目4个、安全性质6个，通过形式化描述，这些功能项和环境项都被引入到形式化模型中，并在模型中建立了安全性质的形式化描述，共成了177条(198减掉需求层21条)证明义务，通过工具验证，模型中所有的证明义务都得到了证明，并且没有发现死锁和不变式违反案例，从而证明了模型的正确性和安全性.

4 设计层和需求层的一致性

通过设计重写后的项目与需求重写后的项目的对应关系可知，设计重写项和需求重写项能够一一对应，这保证了重写后设计和需求的一致性.在Rodin平台下，设计层第0层模型macL1D0直接由需求层最后一层模型macL0R1通过Event-B的refine机制建立，并且模型macL1D0生成的证明义务都得到证明，而且不存在不变式违反情形，从而保证了Event-B模型中设计层和需求层的一致性.原始需求和设计文档、需求和设计重写文档以及Event-B模型间的一致性关系如图9所示.

5 结 论

本文基于Rodin平台，采用Event-B形式化语言，通过需求和设计重写、制定精化策略并逐步精化的方法，对航天嵌入式操作系统SpaceOS2的中断管理模块建立了需求层和设计层形式化模型，将模型检验和定理证明相结合，验证了模型的正确性并且满足安全性质，并且验证了设计模型和需求模型的一致性.

[1] KLEIN G, ELPHINSTONE K, HEISER G, et al. SeL4: formal verification of an OS kernel[J]. ACM Symposium on Operating Systems Principles, 2009:207-220.

[2] KLEIN G, ANDRONICK J, ELPHINSTONE K, et al. comprehensive formal verification of an os microkernel[J]. ACM Transactions on Computer Systems, 2014, 32(1):136-156.

[3] WOODCOCK J, LARSEN P G, BICARREGUI J, et al. Formal methods: practice and experience[J]. ACM Computing Surveys, 2009, 41(4):1729-1739.

[4] CLARKE E M, GRUMBERG O, PELED D. Model checking[M]. MIT press, 1999.

[5] HOARE C A R, JIFENG H. Unifying theories of programming[M]. Englewood Cliffs: Prentice Hall, 1998.

[6] WALKER B J, KEMMERER R A, POPEK G J. Specification and verification of the ucla unix security kernel[J]. Communications of the ACM, 1980, 23(2):118-131.

[7] BEVIER W R. A verified operating system kernel[M].The University of Texas at Austin. 1987.

[8] BIRRELL A D, GUTTAG J V, HORNING J J, et al. Synchronisation primitives for a multiprocessor: a formal specification[C]//The 11thACM Symposium on Operating Systems Principles. ACM, 1987:94-102.

[9] ZHOU D, BLACK P E. Formal specification of operating system operations[C]// Process. IEEE TC-ECBS Working Group WG10.1. New York: IEEE, 2001:69-73.

[10] HOHMUTH M, TEWS H. The VFiasco approach for a verified operating system[J]. Proceedings of the 2nd ECOOP Workshop on Programming Languages and Operating Systems, 2005

[11] SHAPIRO J, DOERRIE M S, NORTHUP E, et al. Towards a verified, general-purpose operating system kernel[C]//FM Workshop on OS Verification. Technical Report 0401005T-1, National ICT Australia. 2004:1-19.

[12] DAUM M, SCHIRMER N W, SCHMIDT M. Implementation correctness of a real-time operating system[C]//Software Engineering and Formal Methods, the 7thIEEE International Conference on Software Engineering and Formal Methods. New York: IEEE, 2009:23-32.

[13] BAUMANN C, BORMER T. Verifying the pikeos microkernel: first results in the verisoft xt avionics project[C]//Doctoral Symposium on Systems Software Verification (DS SSV’09) Real Software, Real Problems, Real Solutions. 2009:20-22.

[14] ELPHINSTONE K, HEISER G. From L3 to seL4 what have we learnt in 20 years of L4 microkernels?[J]. ACM Sigops Symposium on Operating Systems Principles, 2013:133-150.

[15] LIANG H, FENG X, FU M. Rely-guarantee-based simulation for compositional verification of concurrent program transformations[J]. ACM Transactions on Programming Languages & Systems, 2014, 36(1):307-323.

[16] 钱振江. 安全操作系统形式化设计与验证方法研究[D]. 南京: 南京大学, 2013. QIAN Z J. Research on methodology of formal design and verification for security operating system[D]. Nanjing: Nanjing University, 2013.

[17] JASTRAM M, BUTLER P M. Rodin user’s handbook: covers rodin v.2.8[M]. CreateSpace Independent Publishing Platform, 2014.

[18] ABRIAL J R. Modeling in Event-B: system and software engineering[M]. Cambridge University Press, 2010.

[19] LEUSCHEL M, BUTLER M. ProB: An automated analysis toolset for the B method[J]. International Journal on Software Tools for Technology Transfer, 2008, 10(2):185-203.

Formal Modeling and Verification Method of Interrupt-ManagementRequirement and Design Based on Event-B

ZHOU Yukui, YANG Hua, QIAO Lei

(BeijingInstituteofControlEngineering,Beijing100190，China)

With the rapid growth of software complexity, the traditional testing method is gradually difficult to meet the reliability and security requirements of spacecraft operating system. Formal method is gradually becoming an effective guarantee for spacecraft operating system security and reliability. Based on the Rodin platform, using Event-B formal language, through the requirements and design rewrite and formulate the refinement strategy and stepwise refinement method, the requirement layer and design layer formal model is established for the interrupt-management module of the embedded operating system SpaceOS2. Model checking and theorem proving are combined to verify the validity and safety of the model.

interrupt-management; formal verification; Event-B; refinement

*国家自然科学基金资助项目(61632005, 61502031).

2017-03-07

周育逵(1989—)，男，硕士研究生，研究方向为嵌入式操作系统、形式化方法；杨 桦(1969—)，女，研究员，研究方向为高可信操作系统、星载容错计算机；乔 磊(1982—)，男，高级工程师，研究方向为操作系统模型设计、存储管理、文件系统.

TP311

A

1674-1579(2017)03-0071-08

10.3969/j.issn.1674-1579.2017.03.012