在嵌入式系统和各类操作系统中, 中断机制是确保实时响应各类异步事件的常用方法.在处理一个中断的过程中, 通常会出现更紧迫的中断事件请求响应, 因而导致中断嵌套.中断事件的发生具有极大的不确定性, 而且中断的响应与处理往往与硬件密切相关, 因而, 确保中断系统的可靠性和安全性是一项极具挑战性的工作.

形式化验证是一种确保软硬件系统可靠性和安全性的有效方法.定理证明和模型检测是形式化验证方法中的两种关键技术, 主要用来判定一个系统是否具备某种性质.与定理证明相比, 模型检测可以自动化进行.近年来, 很多研究围绕形式化建模和验证中断系统展开.本文主要考虑嵌套中断系统, 这是对文献[1]所做工作的扩展和推广.文献[2]利用多线程系统验证的方法来验证中断系统, 由于中断缺乏形式化语义支持, 所以使用该方法时, 将中断的语义用等价的线程语义来形式化描述.然而, 中断和线程之间的精细的差别使得用线程语义描述中断这个过程变得棘手.文献[3, 4]验证μC/OS-Ⅱ操作系统中的嵌套中断系统, 该方法借助霍尔逻辑^[5]和分离逻辑^[6]建模中断系统, 使用定理证明工具Coq^[7]完成定理证明过程.文献[8]用时间Petri网建模嵌套中断系统, 并将Petri网所建立的系统模型转换为时间自动机^[9], 从而借助时间自动机理论进行模型检测.文献[10]使用iDola语言建模嵌套中断系统, 与文献[8]的方法类似, 验证是通过把iDola语言程序转换为时间自动机完成的.文献[11]直接使用时间自动机建模嵌套中断系统.然而, 在基于时间自动机的模型检测中, 待验证的性质采用LTL^[12]表示, 使得对于周期性性质和区间相关的性质不容易表达^[13].本文是对已有嵌套中断系统验证工作中存在不足的补充, 采用基于MSVL(modeling, simulation and verification language)^{[14, 15]}统一模型检测的方法^[13]来验证嵌套中断系统.该方法为包含任意多中断事件的中断系统提供了有效的形式化语义支持, 从而可以直接建模并验证嵌套中断系统.

MSVL是一种建模仿真和验证各类软硬件系统的语言, 该语言使用投影时序逻辑(projection temporal logic, 简称PTL)^{[14, 15]}定义得到, 是PTL的一个可执行子集.本文使用PTL定义了基本中断模型, 并将该模型推广到建模包含任意多个中断事件的中断系统.接着, 使用定义的中断模型扩充MSVL语言, 同时扩展MSVL语言的模型检测工具^{[13, 16]}, 使其支持对中断语句的处理.这样, 借助MSVL语言以及工具集MSV^[16], 可以实现对包含任意多个中断事件的中断系统的建模仿真与验证.相比于常见的模型检测方法, 基于MSVL的模型检测方法具有以下优势.

(1) 系统建模语言和性质描述语言基于相同的时序逻辑;

(2) 该方法中的性质描述语言有较强的表达能力, 可以描述周期性性质和区间相关的性质^[13].

本文第1节介绍PTL和可执行语言.第2节研究如何使用PTL定义包含任意数量中断事件的中断系统.第3节介绍如何扩展工具集MSV, 使其支持对中断系统的模型检测.第4节使用本文提出的方法建模和验证一个实例, 给出建模和验证的过程以及结果分析.最后一节总结全文, 并对未来研究提出进一步展望.

1 基础知识

本节主要介绍投影时序逻辑^{[14, 15]}和可执行语言^{[14, 15]}.

1.1 投影时序逻辑

语法.令V代表变量集合, Pr代表可数的原子命题集合, D为数据域, B={true, false}为布尔域.PTL的项e和公式ϕ归纳定义如下:

$\begin{align} &e::=v|\bigcirc e|\Theta e|f({{e}_{1}}, ..., {{e}_{m}}) \\ &\phi ::=p|{{e}_{1}}={{e}_{2}}|P({{e}_{1}}, ..., {{e}_{m}})|{{\phi }_{1}}\wedge {{\phi }_{2}}|\neg \phi |\exists v:\phi |\bigcirc \phi |({{\phi }_{1}}, ..., {{\phi }_{m}})\text{ }prj\text{ }\phi \\ \end{align}$

其中, v∈V, $\bigcirc $ 和 $\Theta $ 为时序操作符, f为函数, p∈Pr, P代表谓词, (ϕ₁, …, ϕ_m) prj ϕ为投影公式.当一个公式不包含时序操作符$\bigcirc $, $\Theta $, prj时, 称其为状态公式, 否则为时序公式.

语义.状态s是一组映射:(I_v, I_p), 其中, I_v:V→D', D'=D∪{nil}.这里, nil为无定义, I_p:Pr→B.我们用s[v]和s[p]分别表示变量v和命题p在状态s的取值.区间σ=〈s₀, s₁, …, s_|σ|〉是一个非空的状态序列, 其中, s₀为起始状态, 若σ不为无穷大, s_|σ|为终止状态.|σ|代表σ的长度, 它等于σ的状态个数减1.我们用σ_{(i, j)}(0≤i≤j≤|σ|)表示区间σ上以s_i为起始状态、s_j为终止状态的子区间.令r₁, …, r_h(h≥1)为整数且r₁≤…≤r_h≤|σ|, σ在r₁, …, r_h上的投影构成了一个新区间, 称为投影区间: $\sigma \downarrow ({r_1}, ..., {r_h}) = \langle {s_{{t_1}}}, {s_{{t_2}}}, ..., {s_{{t_l}}}\rangle $, 其中, t₁, …, t_l是r₁, …, r_h的最长严格递增序列, 例如:

〈s₀, s₁, s₂, s₃, s₄〉 $\begin{array}{l} \downarrow \\ \end{array} $ 〈0, 0, 2, 2, 4〉=〈s₀, s₂, s₄〉.

PTL的项和公式的解释定义为四元组I=(σ, i, k, j), 其中, i, k, j是非负整数且0≤i≤k≤j≤|σ|.(σ, i, k, j)表示σ上以s_k为当前状态的子区间s_{(i, j)}.项e的解释I[e]定义如下:

$\begin{align} &\mathcal{I}[v]={{s}_{k}}[v]\in {D}', \\ &\mathcal{I}[\bigcirc e]=\left\{ \begin{array}{*{35}{l}} (\sigma , i, k+1, j)[e], \text{ }如果k <j \\ nil, \text{ }其他情况 \\ \end{array} \right., \\ &\mathcal{I}[\Theta e]=\left\{ \begin{array}{*{35}{l}} (\sigma , i, k-1, j)[e], \text{ }如果k>i \\ nil, \text{ }其他情况 \\ \end{array} \right., \\ &\mathcal{I}[f({{e}_{1}}, ..., {{e}_{m}})]=\left\{ \begin{array}{*{35}{l}} \mathcal{I}[f](\mathcal{I}[{{e}_{1}}], ..., \mathcal{I}[{{e}_{m}}]), \text{ }如果对任意h, 1\le h\le m, \mathcal{I}[{{e}_{h}}]\ne nil \\ nil, \text{ }其他情况 \\ \end{array} \right.. \\ \end{align}$

PTL公式的可满足关系|=定义如下.

●    $\mathcal{I} $|=p当且仅当s_k[p]=true;

●    $\mathcal{I} $ |=e₁=e₂当且仅当$\mathcal{I} $(e₁)=$\mathcal{I} $(e₂);

●   $\mathcal{I} $|=P(e₁, …, e_m)当且仅当$\mathcal{I} $[P]($\mathcal{I} $[e₁], …, $\mathcal{I} $[e_m])=true且$\mathcal{I} $[e₁]≠nil, …, $\mathcal{I} $[e_m]≠nil;

●   $\mathcal{I} $|=ϕ₁∧ϕ₂当且仅当$\mathcal{I} $|=ϕ₁且$\mathcal{I} $|=ϕ₂;

●    $\mathcal{I} $|=¬ϕ当且仅当$\mathcal{I} $|$ \ne $ ϕ;

●    $\mathcal{I} $|=∃v:ϕ当且仅当∃σ', (σ', i, k, j)|=ϕ, 其中, σ与σ'的唯一区别是v的取值可以不同;

●   $\mathcal{I} $|=$\bigcirc $ ϕ当且仅当k < j且(σ, i, k+1, j)|=ϕ;

●   $\mathcal{I} $|=(ϕ₁, …, ϕ_m) prj ϕ当且仅当存在非负整数k=r₀≤r₁≤…≤r_m≤j, 使得(σ, i, r_l-1, r_l)|=ϕ_l(1≤l≤m), 并且对于以下的σ'之一, (σ', 0, 0, |σ'|)|=ϕ:

(a) r_m < j并且$\sigma ' = \sigma \downarrow ({r_0}, ..., {r_m}).{\sigma _{({r_{m + 1}}, j)}};$

(b) r_m=j并且$ \sigma ' = \sigma \downarrow ({r_0}, \ldots , {r_m}).$

如果(σ, 0, 0, |σ|)|=ϕ, 则称公式ϕ在区间σ上可满足, 记做σ|=ϕ.如果存在区间s使得σ|=ϕ, 则称公式ϕ是可满足的.如果对于任意的区间σ, σ|=ϕ, 则称公式ϕ是有效的, 记做|=ϕ.

投影加prj^⊕(projection plus)和投影星$pr{{j}^{\circledast }}$ (projection star)公式是PTL的两个派生公式, 投影加的定义见定义式A1, 投影星$pr{{j}^{\circledast }}$的定义见定义式A2.在A1中, n为任意的正整数或者无穷大; 在A2中, σ表示到达终止状态, 定义为$\sigma \triangleq \neg \bigcirc \text{true} $.由于篇幅限制, PTL的其他派生公式及相应逻辑规则未在本文给出, 可见文献[14, 15].

$\begin{align} &\text{A}1.\text{ }({{\phi }_{1}}, ..., {{({{\phi }_{i}}, ..., {{\phi }_{l}})}^{\oplus }}, ..., {{\phi }_{m}})\text{ }prj\text{ }\phi \triangleq ({{\phi }_{1}}, ..., {{({{\phi }_{i}}, ..., {{\phi }_{l}})}^{n}}, ..., {{\phi }_{m}})\text{ }prj\text{ }\phi . \\ &\text{A}2.\text{ }\begin{array}{*{35}{l}} ({{\phi }_{1}}, ..., {{({{\phi }_{i}}, ..., {{\phi }_{l}})}^{\circledast }}, ..., {{\phi }_{m}})\text{ }prj\text{ }\phi \triangleq ({{\phi }_{1}}, ..., \varepsilon , ..., {{\phi }_{m}})\text{ }prj\text{ }\phi \vee ({{\phi }_{1}}, ..., {{({{\phi }_{i}}, ..., {{\phi }_{l}})}^{\oplus }}, ..., {{\phi }_{m}})\text{ }prj\text{ }\phi \\ \end{array}. \\ \end{align}$

1.2 可执行语言MSVL

语法和语义. MSVL^{[14, 15]}是PTL的一个可执行子集, 它支持整型、浮点型、字符、字符串、指针、数组、结构体等数据类型^[17]以及函数调用^[18].它由表达式和基本语句构成.算术表达式e和布尔表达式b定义如下.

$\begin{array}{l} e:: = c|v|\bigcirc e|\Theta e|f({e_1}, ..., {e_m})\\ b:: = {\rm{true}}|{e_1} = {e_2}|{e_1} < {e_2}|\neg b|{b_1} \wedge {b_2} \end{array}$

其中, c为常量, v为变量, f表示函数.MSVL语言的语句及语法定义见表 1.

这些语句的定义及语义见文献[14, 15], 本文仅介绍其直观含义.终止语句empty表示程序到达终止状态.赋值语句v$\Leftarrow $ e表示在当前状态下将v的值置为e, 且将记录v是否被赋值的命题变元p_v置为true.赋值语句v:=e表示在长度为1的区间上, 在下一状态将v的值置为e, 且将记录v是否被赋值的命题变元p_v置为true.Oϕ表示ϕ从下一状态开始执行.ϕ₁∧ϕ₂表示同时执行f₁和ϕ₂.ϕ₁∨ϕ₂表示执行ϕ₁或者ϕ₂.ϕ₁; ϕ₂表示先执行ϕ₁, ϕ₁结束后继续执行f₂.ϕ₁||ϕ₂表示ϕ₁和ϕ₂并行执行.len(n)表示长度为n的区间, skip表示长度为1的区间.keep(ϕ)表示从当前状态开始, ϕ在除终止状态外的每个状态上执行.frame(ϕ)表示如果变量v未被赋值, 那么它的值保持不变.条件语句和循环语句的含义与传统的程序设计语言相同.await(b)表示等待条件b成立, 且在b成立时结束等待.

基于MSVL的统一模型检测.该过程的原理如下:将一个系统建模成MSVL程序M, 待验证的性质描述成MSVL程序M', 为了判断系统是否满足这一性质, 我们需要证明公式M→M'的有效性.由于¬(M→M') $\equiv $ M∧¬M', 等价地, 我们判断公式M∧¬M'是否不可满足.对每一个σ|=M∧¬M', σ确定了一条系统违背给定性质的反例.因而, 模型检测问题被转化为判断形如M∧¬M'的PTL公式的可满足性问题.由于模型M和性质M'都是PTL公式, 所以这种模型检测方法被称作统一模型检测.判定PTL公式M∧¬M'的可满足性问题涉及构造MSVL程序的范式、范式图以及寻找反例路径等过程, 可见文献[13].以下给出MSVL程序的范式的定义.在文献[14, 15]中, 已证明所有的MSVL语句都可以化为范式.

范式(normal form). MSVL程序ϕ的范式为$ \phi \equiv \vee _{i=1}^{{{n}_{1}}}{{\phi }_{ei}}\wedge empty\vee \vee _{j=1}^{{{n}_{2}}}{{\phi }_{cj}}\wedge \bigcirc {{\phi }_{fj}}, $其中, n₁和n₂为非负整数, n₁+n₂≤1;ϕ_ei和ϕ_cj为true或者状态公式; ϕ_fj为MSVL程序.

2 中断及嵌套中断系统的建模

在嵌入式系统及操作系统中, 中断的优先级往往高于普通任务.这样, 普通任务会因中断请求而暂停执行, 直到中断事件处理完毕后恢复执行.在包含多个中断事件的系统中, 系统按照中断事件的重要程度为其分配优先级.系统在响应一个中断请求的时候, 可能被更高优先级的中断事件中断, 从而引起嵌套中断.图 1展示了一个嵌套中断场景, 其中, X为系统主程序, 执行过程中随时可能被中断事件irq1, irq2, irq3和irq4(优先级依次升高)中断.系统执行对应的中断服务程序Handler1~Handler4来响应中断请求.针对中断系统模型, 本节先使用投影时序逻辑PTL定义只含一个中断事件的中断系统, 建立了基本中断模型; 然后, 针对包含任意个数中断事件的(嵌套)中断系统, 给出了基于PTL的建模方法.

2.1 基本中断模型

我们使用语句ϕ when (p, b) do ϕ'表示只包含一个中断事件的中断系统的模型, 简称基本中断模型.其中:公式ϕ代表中断系统中的主程序; p是一个辅助定义的命题变元; b为布尔表达式, 表示是否可响应中断请求; 公式ϕ'为中断服务程序.在定义中, 我们需要确保中断语句f when (p, b) do ϕ'随着主程序ϕ的执行结束而结束.基本中断模型的定义如下:

$\phi \text{ when }(p, b)\text{ do }{\phi }'\triangleq ({{(\text{if }b\text{ then }{\phi }'\text{ else }skip)}^{\circledast }}, p\wedge \varepsilon )\text{ }prj\text{ }(\phi ;p\wedge \varepsilon ))\wedge halt(p).$

该定义式包含一个投影星($pr{{j}^{\circledast }}$)公式, 它是PTL中的投影结构的一个变种.在定义式中, p是辅助定义的命题变元, 便于投影结构左边和右边语句的执行能够同时结束.halt(p)是PTL的派生公式, 它表示在任意时刻, p为真等价于区间结束.基于p, 投影语句与halt(p)的合取实现了投影符号(prj)两边的公式的同时结束, 从而确保了中断语句随着主程序ϕ的执行结束而结束.显然, ϕ when (p, b) do ϕ'表示主程序ϕ在执行的过程中, 一旦需要响应中断请求, ϕ将会暂停执行, 让出执行权使得中断服务程序ϕ' 执行.当ϕ'执行完后, 返回主程序ϕ的中断点继续执行.图 2给出了中断语句ϕ when (p, b) do ϕ'的执行示意图, 其中:图 2(a)为主程序执行过程中无需响应中断请求的情况, 图中垂直虚线连接的状态为投影状态, skip表示主程序ϕ的执行未被中断; 图 2(b)表示在ϕ执行的过程中, 有两次响应中断请求的过程, 在这期间ϕ'的执行使得主程序ϕ暂停执行.

2.2 嵌套中断系统模型

嵌套中断系统的模型基于基本中断模型定义而成.我们用如下析取式表示包含n个中断事件(优先级各不相同)的中断系统模型: $\vee _{i=1}^{n}interrupt(Q, {{r}_{i}}, {{H}_{i}}), $其中,

●    Q代表中断系统的主程序;

●  布尔类型变量r_i代表中断事件i(i=1, …, n)是否请求响应:若请求响应, r_i=1;否则, r_i=0.且r_i的下标越大, 所代表的中断事件的优先级越高;

●    H_i代表中断事件i的中断服务程序;

●    interrupt(Q, r_i, H_i)表示主程序Q在响应中断事件i时的嵌套中断模型, 它基于基本中断模型定义而成.

以n=4为例, interrupt(Q, r_i, H_i)(i=1, 2, 3, 4)的定义如下:

$ \begin{align} &interrupt(Q, {{r}_{1}}, {{H}_{1}})\triangleq Q\text{ when }(p, {{r}_{1}})\text{ do }(\vee _{i=2}^{4}interrupt({{H}_{1}}, {{r}_{i}}, {{H}_{i}})), \\ &interrupt(Q, {{r}_{2}}, {{H}_{2}})\triangleq Q\text{ when }(p, {{r}_{2}})\text{ do }(\vee _{i=3}^{4}interrupt({{H}_{2}}, {{r}_{i}}, {{H}_{i}})), \\ &interrupt(Q, {{r}_{3}}, {{H}_{3}})\triangleq Q\text{ when }(p, {{r}_{3}})\text{ do }(interrupt({{H}_{3}}, {{r}_{4}}, {{H}_{4}})), \\ &interrupt(Q, {{r}_{4}}, {{H}_{4}})\triangleq Q\text{ when }(p, {{r}_{4}})\text{ do }{{H}_{4}}, \\ \end{align} $

其中,

$ \begin{align} &interrupt({{H}_{1}}, {{r}_{2}}, {{H}_{2}})\triangleq \text{ }{{H}_{1}}\text{ when }(p, {{r}_{2}})\text{ do }(\vee _{i=3}^{4}interrupt({{H}_{2}}, {{r}_{i}}, {{H}_{i}})), \\ &interrupt({{H}_{1}}, {{r}_{3}}, {{H}_{3}})\triangleq Q\text{ when }(p, {{r}_{3}})\text{ do }(interrupt({{H}_{3}}, {{r}_{4}}, {{H}_{4}})), \\ &interrupt({{H}_{1}}, {{r}_{4}}, {{H}_{4}})\triangleq {{H}_{1}}\text{ when }(p, {{r}_{4}})\text{ do }{{H}_{4}}, \\ &interrupt({{H}_{2}}, {{r}_{3}}, {{H}_{3}})\triangleq {{H}_{2}}\text{ when }(p, {{r}_{3}})\text{ do }(interrupt({{H}_{3}}, {{r}_{4}}, {{H}_{4}})), \\ &interrupt({{H}_{2}}, {{r}_{4}}, {{H}_{4}})\triangleq {{H}_{2}}\text{ when }(p, {{r}_{4}})\text{ do }{{H}_{4}}, \\ &interrupt({{H}_{2}}, {{r}_{1}}, {{H}_{1}})\triangleq {{H}_{2}}interrupt({{H}_{3}}, {{r}_{4}}, {{H}_{4}})\triangleq {{H}_{3}}\text{ when }(p, {{r}_{4}})\text{ do }{{H}_{4}}, \\ &interrupt({{H}_{3}}, {{r}_{i}}, {{H}_{i}})\triangleq {{H}_{3}}\text{ }(i <3), \\ &interrupt({{H}_{4}}, {{r}_{i}}, {{H}_{i}})\triangleq {{H}_{4}}\text{ }(i <4). \\ \end{align} $

需要注意的是:在有中断请求发生的情况下, 即使是多个中断嵌套, 同一时刻也只有一个中断服务程序在执行, 不存在一个主程序既被中断事件r_i中断, 又被事件r_j(i≠j)中断.中断事件的模型析取式中的多个interrupt()有且仅有一个为真.以interrupt(Q, r₁, H₁)定义式中的$\vee _{i=2}^{4}interrupt({{H}_{1}}, {{r}_{i}}, {{H}_{i}})$为例, 当interrupt(H₁, r_i, H_i)(i=2, 3, 4)为真时表示为p_i, 否则表示为¬p_i.那么$\vee _{i=2}^{4}{{p}_{i}}$应满足表 2所示的真值表.即, $\vee _{i=2}^{4}{{p}_{i}}$应该满足p₂∧¬p₃∧¬p₄∨¬p₂∧p₃∧¬p₄∨¬p₂∧¬p₃∧p₄.对于其他情况, 与此类似.

图 3为含有4个中断事件的中断系统未发生中断请求时的模型图, 主程序Q的执行生成了状态序列s₁, …, s₁₆.图 4为发生中断请求时的模型图.如图所示:在多个中断事件同时请求响应的情况下, 它们将按优先级高低的顺序依次被响应.例如:主程序执行到状态s₂时, 中断请求r₁, r₂, r₃同时到达, 而中断请求r₃优先被响应.且图 4包含了低优先级的中断服务程序被高优先级的中断事件抢占的情况.例如:在状态s₅和s₆之间, 中断响应程序H₁中断了主程序的执行; 随后, H₁被中断响应程序H₃中断.

3 MSVL解释器的扩展

MSVL解释器的架构如图 5所示.建模、仿真和验证是MSVL解释器的三大功能模块.建模功能可以构造出输入程序的范式图^[13], 它显示了程序的状态空间; 仿真功能可以得到程序的一条执行路径; 验证功能验证程序是否满足指定的性质, 若不可满足, 给出一条反例路径.这3种功能的实现主要借助于对程序的状态化简和区间化简.其中, 状态化简对MSVL程序的语法树进行表达式求值和化范式, 状态化简完成后对程序做区间化简, 从而确定下一状态的要执行的程序.

为使得MSVL解释器支持对含中断结构的程序的建模仿真和验证, 我们在MSVL解释器中增加对中断语句的处理.该工作主要涉及对中断语句构造语法树和化范式, 其他的处理可以直接调用解释器的内部功能.

3.1 语法树的构造

基本中断语句ϕ when (p, b) do ϕ'的语法树结构如图 6所示, 根节点代表语句类型, 即中断语句, 3个子节点分别对应主程序的语法树、中断处理的条件以及中断服务程序的语法树.由于p是辅助中断语句定义的命题变元, 没有实际含义, 可不做处理, 故在语法树中省略了对p的表示.

3.2 状态化简

状态化简涉及到对程序化范式以及对表达式(算术表达式和布尔表达式)求值, 该过程见文献[15].

假设中断语句ϕ when (p, b) do ϕ'中主程序ϕ的范式为ϕ$\equiv $ϕ_e∧empty∨ϕ_c∧df_f, ϕ'的范式为

${\phi }'\equiv {{{\phi }'}_{e}}\wedge empty\vee {{{\phi }'}_{c}}\wedge \bigcirc {{{\phi }'}_{f}}$

图 7给出了在化简中断语句ϕ when (p, b) do ϕ'时语法树的变化情况, 其中,

●  图 7(ⅰ)代表ϕ when (p, b) do ϕ' 的语法树;

●   图 7(ⅱ)为ϕ_e∧empty的语法树;

●   图 7(ⅲ)为ϕ_c∧d(ϕ_f when (p, b) do ϕ' )的语法树;

●   图 7(ⅳ)为${{\phi }_{c}}\wedge {{{\phi }'}_{c}}\wedge \bigcirc ({{{\phi }'}_{f}};{{\phi }_{f}}\text{ when }(p, b)\text{ do }{\phi }')$的语法树.

状态化简中断语句时, 首先执行程序ϕ:

●   若ϕ结束, 则中断语句执行结束, 法树的变换如图 7(ⅱ)所示;

●  若ϕ未结束, 则判断中断响应条件b是否成立:若不成立, 执行ϕ, 使得语法树变为图 7(ⅲ)所示的形式; 否则, 执行ϕ'且语法树变为图 7(ⅳ)所示的形式.

在语法树(ⅲ)和(ⅳ)中, 以NEXT_STA为根节点的子树为下一状态语法树.

4 实验与分析

本节建模并验证图 8所示的中断系统实例.主程序包含一个局部变量sum, 主程序不断对sum的值加1, 直到sum的值等于100或者全局变量timerCount的值变为0时, 结束对sum的自增操作, 并返回sum的值.主程序在执行过程中, 随时可能被两个中断事件中断:当发生中断事件1时, 触发中断服务程序ISR1的执行, 全局变量timerCount的值被减1;当发生中断事件2时, 触发中断服务程序ISR2的执行, 使得全局变量timerCount的值被重设为20.注意, 这里, 中断事件2的优先级高于中断事件1.

我们的目标在于验证主程序的数据安全性, 即:中断服务程序的执行不改变主程序里变量的值, 即sum的值.为验证这个性质, 接下来我们用MSVL建模中断系统实例并描述待验证性质.

4.1 建模

我们将图 8所示的中断系统实例的嵌套中断模型记做M, 其中, 变量的声明与初始化模块用DcInt表示, 主程序的形式化模型用Q表示, 中断服务程序ISR1和ISR2的形式化模型分别用H₀, H₁表示.借助于第2节提出的建模方法, M可被定义为如下形式.

●    M $\triangleq $ DeInt; (interrupt(Q, r[0], H₀)∨interrupt(Q, r[1], H₁));

●    interrupt(Q, r[0], H₀)@Q when (p, r[0]) do (interrupt(H₀, r[1], H₁));

●    interrupt(H₀, r[1], H₁)@H₀ when (p, r[1]) do H₁;

●    interrupt(Q, r[1], H₁)@Q when (p, r[1]) do H₁.

其中, r[j]代表事件j+1(j=0, 1)请求响应且系统允许中断.M中的各个模块的MSVL代码如图 9所示.在变量的声明与初始化模块DcInt中, 各变量的含义如下.

●   sum和timerCount为中断系统实例中的变量;

●  数组iEv代表发生的事件, iEv[0], iEv^[1]分别表示中断事件1和中断事件2, 若中断事件j+1请求处理, 则iEv[j]=1;否则iEv[j]=0(j=0, 1);

●   ie表示是否允许中断, 若允许中断, ie=1;否则, ie=0.

在允许中断且没有更高优先级中断时, 中断事件iEv[j]的请求将得到响应, 并且isr[j]被设为1.在该中断事件处理完毕后, isr[j]被设为0.变量inv1和inv2是为辅助性质验证引入的变量, 分别记录每次执行中断服务程序前变量sum和timerCount的值.

4.2 验证

本节借助MSVL解释器仿真和验证模型M.表 3列出了3个输入实例的模型, 其中:输入1对应先发生了一次中断事件1, 接着发生了一次中断事件2的情况, 其时间间隔为1个时间单位; 输入2描述在第4个时间单位, 中断事件1和中断事件2同时请求响应的情况; 输入3描述在第4个时间单位, 中断事件1和中断事件2同时请求响应, 随后, 过了25个时间单位, 它们分别又请求一次响应的情况.

本文验证中断系统中主程序的数据安全性性质.在主程序执行过程中, 主程序中的一些变量不可以被中断服务程序改变, 即:任何时候主程序被中断, 在中断返回前后, 这些变量的值都是一致的.在M中, 变量sum为局部变量, 因而在主程序被中断转而执行中断服务程序的过程中, 该变量的值不允许被中断服务程序修改.为描述这个性质, 我们用变量inv1记录在进入中断服务程序前的sum值, 并定义命题p₀, p₁, q₁, q₂为如下形式:

define p₀: isr[0]=1; define p₁: isr^[1]=1; define q₁: sum=inv1; define q₂: timerCount=inv2.

借助以上命题, 变量sum和timerCount的数据安全性性质分别记为Pr₁和Pr₂, 则它们可用PTL公式定义为如下形式.

●    Pr₁ $\triangleq \square $ ((p₀∨p₁)→q₁);

●   Pr₂$\triangleq \square $((p₀∨p₁)→q₂);

使用扩展后的MSVL解释器对表 3的输入进行验证, 验证结果见表 4.

对于所给输入, 性质Pr₁有效, 而Pr₂被违背.由于仅主程序可以访问变量sum, 所以在响应中断服务程序的过程中, 该变量的值是不允许被改变的, 验证结果与实际相符.对于变量timerCount, 由于中断服务程序ISR1和ISR2都要访问且修改该变量, 所以在响应中断的过程, 该变量的值被改变, 验证结果也与实际相符.

5 结束语

本文提出一种建模和验证嵌套中断系统的方法.

●  首先, 为中断系统提出了基于投影时序逻辑的形式化定义, 并将这种定义应用到建模包含任意个中断事件的中断系统上, 从而得出嵌套中断系统基于投影时序逻辑的形式化模型;

●  其次, 使用定义的中断语句扩充MSVL语言, 使得MSVL语言支持对嵌套中断系统的建模;

●  再次, 扩展了MSVL解释器, 为建模仿真和验证包含任意多中断事件的中断系统提供了工具支持, 从而实现了嵌套中断系统基于MSVL的统一模型检测;

●  最后, 使用一个实例展示如何使用本文提出的方法建模和验证嵌套中断系统.使用本文提出的方法, 方便建出简洁的系统模型, 且与PLTL^[12]相比, MSVL对性质的描述更完整.

在今后的工作中, 我们将研究如何对实际应用中的中断系统建立MSVL模型.由于中断程序往往是由C语言或者汇编语言编写的, 我们将结合文中所提出的模型, 并借助C语言以及汇编语言到MSVL语言的转换技术辅助建模具体应用中的中断系统.