信息-物理融合系统 (cyber-physical system, 简称CPS)^[1]是一种新型的复杂嵌入式系统计算方式, 其运行融合了计算过程和物理过程, 两者之间具有密切的交互与影响.与传统的信息系统或物理系统相比, CPS系统具有显著的不同特征.例如, 与嵌入式系统相比, CPS需要更多对物理实体的可控性; 与物联网/传感网相比, CPS更强调物理节点中融入复杂的计算过程以及对物理环境变化的适应性; 与混成系统 (hybrid system) 相比, CPS不仅仅是简单包含离散过程和连续过程的系统, 而是需要二者更加深入的融合和可控, 以及更高的精确性和适应性.

随着信息技术在现实世界中更加广泛、深入的应用, 智能化程度不断提升, 系统规模和复杂度日趋增大, 在具有信息-物理紧密耦合特点的新型嵌入式系统中, 嵌入式软件的功能比重急剧上升, 作用更加突出.国际上在军事、航空、航天、医疗、交通等关键应用领域, 由核心控制应用软件设计缺陷所带来的系统失效造成了巨大的损失, 已经引起了人们的高度重视, 我国在卫星、飞机等重点型号研制过程以及投入使用后所发生的异常事件或重大事故中有不少也与其嵌入式软件相关.不断发生的控制软件错误或失效所引发的事故使人们逐渐认识到, 在系统复杂性较高的情况下, 面对CPS这一新型体系结构, 常规的软件工程方法和软件评测手段不能解决嵌入式控制软件安全性设计深层次的问题.

因此, 作为安全攸关的系统, 需要引入形式化验证方法来保证嵌入式控制应用程序的安全性.模型检验作为一种形式化验证技术, 已经在硬件设计和协议实现方面取得成功的应用.随着抽象、符号化等技术的发展, 模型检验逐渐发展到对源代码进行验证.人们研制了数个验证工具原型, 包括CBMC^[2], CPAchecker^[3], 微软的SLAM^[4]项目, 加州大学伯克利分校的BLAST^[5], 美国国家航空航天局开发的JPF^[6], 美国贝尔实验室的SPIN^[7]等.目前将模型检验技术应用于软件源程序的验证是当今嵌入式系统前沿领域的热门研究内容.

面向CPS的自主控制应用程序的运行一般包含感知 (sensing)、控制应用 (controlling) 和实施 (actuating) 这3个过程.这3个过程形成了控制器软件的控制环路 (control loop) 或反馈环路 (feedback loop).而控制器应用软件是这类系统的核心.它依据传感器信号来调整发送至作动器的输出信号, 以改变受控对象 (plant) 状况.由控制器软件构成的闭环控制系统如图 1所示, 其运行既包含连续动态行为 (受控对象) 又包含离散动态行为 (控制应用软件), 系统的状态空间由离散变量和连续变量共同刻画.

目前相关研究如下:文献[8, 9]提出构造系统的时间自动机模型使用UPPAAL间接对控制软件进行了应用验证; 文献[10, 11]只是针对系统模型利用模型检验和定理证明技术来验证; 文献[12-14]只是针对软件实现的控制器的进行了分析, 基于符号执行技术提出了一种计算软件控制性能的方法; 文献[15]提出了一种控制闭环分析方法, 通过集成一个显示的模型检验工具检查控制器软件和Simulink去仿真运行受控对象; 文献[16]提出了一个验证框架, 通过模型转换将Simulink/Stateflow转换为统一的中间表示, 然后基于中间表示做符号执行.文献[17, 18]都对整个控制闭环做了静态分析, 包括控制器程序和受控对象, 基于可达性分析对系统某些属性进行了验证, 并且只能处理定点计算.

目前, 控制应用类软件模型检测主要存在以下两个问题.

(1) 如何构建系统属性的规约.目前的源程序验证工具主要采用基于断言的属性规约描述, 在所需验证的程序位置加入assert (expression) 语句, 基于可达性判断该断言在所有执行路径下是否成立.这种基于断言的属性规约具有一定的局限性, 它无法表达时序、活性 (livness) 等属性.

(2) 如何有效构建控制环路验证模型以支持各种变化的模型检验.系统中控制应用程序和受控对象之间具有时间交互特性, 它们消耗资源并同时影响整个系统的行为.然而控制系统中的大规模复杂异构性、不确定性以及计算过程同步或异步管理需求导致系统的行为越来越复杂, 问题的规模随之急剧增加, 从而影响了可验证系统的规模, 而这也正是著名的组合状态空间爆炸问题.

针对验证这类需要不断地与物理过程交互从而共同完成系统功能的控制应用程序, 本文在已有研究的基础上^[19], 基于自动机理论提出了控制环路的验证模型及其优化验证算法:将控制应用C程序抽象成下推系统, 受控对象被抽象成混成自动机, 基于控制任务周期分析, 在各类自动机的变迁关系添加同步标记, 通过将各自成员进行笛卡尔乘积构造出系统组合后的乘积自动机.基于有界模型检验 (bounded model checking, 简称BMC)^[20]技术, 将验证模型k步内行为采用布尔约束编码, 然后利用SAT/SMT方法来寻找此布尔约束集的可行解, 从而判定系统在k步内行为是否有不满足规约的情况.针对组合状态空间爆炸问题, 通过偏序规约等手段化简模型规模, 并结合虚拟仿真提出了综合虚拟仿真和形式化验证相结合的方法.

本文采用线性时序逻辑LTL (linear temporal logic)^[21]作为模型属性的规约语言, 通过定义在物理连续变量上的布尔表达式描述物理过程, 而后将LTL性质规约公式转换为Büchi自动机, 即将性质分解为与其等价的一组断言, 然后再将这组断言插装到控制应用程序程序的适当位置, 根据断言的违反情况即可判断出性质的满足情况.运行时验证考虑控制应用这样的非终止程序, 在任何时刻只能获得当前执行的一个有穷状态前缀, 针对有穷路径基于四值语义^[22]进行判断.

本文将探讨控制应用程序协同验证方法.本文第1节简述控制应用程序的特点并分析控制任务的时间周期.第2节描述系统验证属性.第3节描述系统验证模型.第4节描述验证算法.第5节简述工具原型的设计.第6节给出实验结果, 并对实验结果加以分析.最后, 第7节对本文加以总结, 并指出进一步的工作方向.

1 面向CPS的控制应用程序分析 1.1 控制应用程序特点

C语言是目前控制应用程序通常使用的编程语言, 因此本文主要针对使用C语言编写的控制应用程序 (如图 2所示).由于运行环境、实现功能等因素, 嵌入式自主控制应用软件具有一些固有特性, 与通用软件相比, 它需要更多的对物理实体的可控性.这就增加了系统设计与功能、性能验证的难度, 其中时间和并发操作是系统复杂性的主要来源.控制应用程序的主要特点.

(1) 物理交互性.控制应用程序能够从物理环境中监测相关数据, 并对数据进行计算, 然后根据控制逻辑通过作动器作用于物理环境.此类系统通过计算过程和物理过程相互影响的反馈循环实现这两者的深度融合和实时交互, 以安全、可靠、高效和实时的方式监测或者控制一个物理实体.这使得嵌入式系统软件的验证必须考虑物理过程的影响, 而计算过程和物理过程的同步过程和异步过程的交织不仅增加了软件设计的复杂度, 也极大地增加了验证的难度.

(2) 时间约束性.在嵌入式系统中, 某一个任务的正确性不仅取决于其功能和行为特性, 还依赖于时间约束特性.这种严格的实时性要求使得诸如航空航天、武器控制、医疗设备等具有高安全可靠要求的嵌入式软件开发从需求分析、设计实现、验证测试均必须显式地考虑时间约束.不仅要验证软件的功能, 而且要验证任务的执行时间.

(3) 存在位操作、float/double等底层数据类型.针对浮点等底层数据类型, 主要是计算精度问题, 目前主要的做法有两种:近似和精确求解.近似目前有过近似 (over-approximate) 和近似 (under-approximate) 两种方法.常用的过近似方法是区间计算 (interval arithmetic), 区间计算将每个变量x定义在一个区间$[\underset{\raise0.3em\hbox{$\smash{\scriptscriptstyle-}$}}{x}, \bar x], $然后在变量的算术运算过程中将区间加入运算, 在不断地迭代过程中有可能是最后结果的区间变得过大而失去意义.如$x \in [1, 3], $ $y \in [5, 7], $ x+y通过区间计算后x+y∈[6, 10].仿射计算 (affine arithmetic) 是近似方法, 它将每个变量x定义为一个多项式$x = {x_0} + {x_1} \cdot {\varepsilon _1} + {x_2} \cdot {\varepsilon _2} + ... + {x_k} \cdot {\varepsilon _k}, $${\varepsilon _1}, {\varepsilon _2}, ..., {\varepsilon _k} \in [-1, 1]$是误差.同样的例子, x=3+e₁, y=5+ε₁, x+y∈8+ω×ε₂, 相对于区间计算, 这样的结果更有价值, 但是计算开销也比较大.精确求解是通过建立位模型 (bit-vector model) 和按位复写 (bit-blasting) 来实现, 这样产生的表达式非常精确, 但是计算开销相对于近似方法会大很多.本文是采用精确求解方法, 求解过程参考Clarke等人的工作^[1].

如图 2所示是一个控制应用程序的典型结构.控制应用程序中存在控制循环, 在每次控制循环中, 首先从传感器读取数据完成A/D转换, 然后基于采样数据计算控制指令, 最后将控制指令写入作动器完成D/A转换.因为对程序中所有的循环加了上界, 所以程序循环边界 (loop bound) 是可知的, 程序必然是终止的, 这是和其他类型程序相比的一个特点.以while循环为例来演示如何将其展开, 其他循环的展开方式类似.while循环的一次展开过程如下:while (s) L; ⇒if (s){L; while (s) L; }.在已经设定上界为n的情况下, 我们将上述循环展开n次, 并在最后一次循环展开加入一个断言来表示, 即assert (!s).

1.2 控制任务周期分析

采样器通过一定时间间隔 (控制周期) 的采样把连续的偏差信号转换成离散信号, 由控制应用程序对它进行适当的变换, 以满足控制的需要, 最后通过保持器再将数字控制器输出的离散控制信号转换成连续的控制信号去控制被控对象.周期性任务的时序关系^[23]如图 3所示, 采用固定控制周期, 控制周期时刻t_k=T×k, 其中, T是控制时间间隔, k是控制次数.t_i和t_o分别表示A/D和D/A转换完成的周期时刻.

由于操作系统任务调度的阻塞和抢占, 所以用L_s表示采样延迟时间, 即实际任务的采样时刻可能会被延迟L_s一段时间.由于调度策略的动态变化使得采样延迟时间并不固定, 我们用J_s表示采样抖动, 并用最小延迟时间和最大延迟时间定义抖动的范围, 即J_s∈[min L_s, max L_s].

在完成计算和可能的任务抢占之后, 控制应用程序开始通过D/A转换发出控制信号, 我们用L_io表示输入/输出延迟时间.由于优先级抢占的调度策略和控制器计算执行时间的不定使得输入/输出延迟时间并不固定, 我们用J_io表示输入/输出抖动, 并用最小延迟时间和最大延迟时间定义抖动的范围, 即J_io∈[min L_io, max L_io].

我们假设${t'_i}$和${t'_o}$分别表示A/D和D/A转换的设计完成时刻.因此A/D转换完成的实际时刻$t = {t'_i} + {J_s}, $D/A转换完成的实际时刻${t_o} = {t'_o} + {J_{io}}.$A/D转换的延迟可能会对控制应用程序的执行产生影响, 即在不同的采样值可能会导致程序的执行路径不一样, 而D/A转换的延迟可能会对受控对象的执行产生影响, 尤其当前后两个控制周期的控制命令不一样时, 这决定了从何时刻开始受控对象开始在新的控制指令下运行.因此, 在本文的研究中将考虑不同情况下延迟对整个系统的影响.

2 验证性质描述

模型检验通常关注系统两个方面的性质:安全性 (safety) 和活性 (livness).

(1) 安全性 (safety), 即Gφ, 坏的事情永远不会发生.安全性可以转化为可达性分析, 即通过可达性分析看是否存在一条路径从初始状态到达这个不安全的状态.

(2) 活性 (livness), 即G(p→Fφ), 是另一类功能性要求, 即好的事情总会发生.

本文使用LTL描述系统属性, 然后将要验证的断言添加到控制应用程序中.通过定义在物理连续变量上的布尔表达式描述物理过程, 使用LTL描述控制应用程序的离散事件和受控对象的连续时间的时序关系, 例如一个活性属性规约, G({Rotary.Velocity > T}→F{Actuator.FanVoltage}=fullNeg), 当转盘的角速度超过限制T时, 控制器最终会将风扇的电压设为fullNeg.这条规约涉及连续变量Rotary.Velocity的值, 以及离散控制变量Actuator. FanVoltage的值.

LTL标准语义是定义在无穷路径上, 针对有穷轨迹.文献[22]提出了LTL四值语义的思想.

定义1.假定φ∈LTL, i∈ℕ表示序列中的一个位置, $u = {u_0}{u_1}...{u_n} \in {\Sigma ^ * }$为有穷状态序列, $\omega \in {\Sigma ^\omega }$为无穷状态序列, uⁱ从序列中的第i个位置开始的有限后缀 (${u^i} = {u_i}{u_{i + 1}}{u_{i + 2}}...{u_{n-1}}, $其中, i < n, 如果i≥n, 则为ε), a^w表示只由$a \in \Sigma $所组成的无限路径, ${\left[{u \vDash \varphi } \right]_\omega }$表示$\left[{u \vDash \varphi } \right]$是定义在无穷路径ω上的, 那么LTL公式的四值语义被定义如下:

$ {{\rm B}_4} = \{ {\rm T}, {{\rm T}^P}, \bot, { \bot ^P}\}, \bot \subseteq { \bot ^P} \subseteq {{\rm T}^P} \subseteq {\rm T}, \bar \bot = {\rm T}和\overline {{ \bot ^P}} = {{\rm T}^P}, $

$ {\left[{u \models \varphi } \right]_B} = \left\{ \begin{array}{l} {\rm T}{\rm{ iff }}\forall \omega \in {\Sigma ^\omega }, {\rm{ }}{\left[{u \models \varphi } \right]_\omega } = {\rm T}\\ {{\rm T}^P}{\rm{ iff }}{\left[{uu_{n-1}^\omega \models \varphi } \right]_\omega } = {\rm T} \wedge \exists \omega \in {\Sigma ^\omega }, {\rm{ }}{\left[{u\omega \models \varphi } \right]_\omega } = \bot \\ \bot {\rm{ iff }}\forall \omega \in {\Sigma ^\omega }, {\rm{ }}{\left[{u\omega \models \varphi } \right]_\omega } = \bot \\ { \bot ^P}{\rm{iff }}{\left[{uu_{n-1}^\omega \models \varphi } \right]_\omega } = \bot \wedge \exists \omega \in {\Sigma ^\omega }, {\rm{ }}{\left[{u\omega \models \varphi } \right]_\omega } = {\rm T} \end{array} \right.. $

3 系统验证模型

软件源程序直接进行模型检验的基础是模型抽象, 即从程序中抽象得到有限状态空间模型.下推系统 (pushdown system, 简称PDS)^[24]为带递归的程序提供了一个理想的执行模型, 但是下推系统并不接受输入.在一个控制闭环中, 受控对象的行为可能会影响软件的执行, 例如采样.因此, 下推系统需要扩展, 即要接受受控对象的输入.基于已有的研究基础^[19], 带标记的下推系统 (labeled pushdown system, 简称LPDS) 的定义如下.

定义2.带标记的下推自动机是具有如下形式的五元组$\left( {I, G, \mathit{\Gamma }, \Delta, \left\langle {{g_0}, {\omega _0}} \right\rangle } \right), $其中各元素的含义如下.

I:输入字母表的有限集合.

G:状态的有限集合.

Γ:堆栈字母表的有限集合.

D:$\Delta \subseteq (G \times \mathit{\Gamma } ) \times I \times (G' \times {\mathit{\Gamma } ^*})$是状态迁移的集合, 表示为$\langle (G \times \mathit{\Gamma } ), I, (G' \times {\mathit{\Gamma } ^*})\rangle, $迁移发生是指输入标记τ时, 发生从源状态 (G×Γ) 到目标状态 (G'×Γ*) 的转移, 记作$\left\langle {g, \gamma } \right\rangle \mathop \to \limits^\tau \left\langle {g', \omega } \right\rangle \in \Delta .$τ可以缺省, 此时τ为空, 表示无条件迁移.

$\left\langle {{g_0}, {\omega _0}} \right\rangle :$初始状态.

带标记的下推系统LPDS的状态为一个二元组s=〈g, ω〉, 其中, g∈G, ω∈Γ, 系统轨迹则是由初始状态经变迁所构成的状态序列.

混成系统通常采用混成自动机 (hybrid automata, 简称HA)^[25]来建模, 混成自动机是在状态机基础上进行实时连续变量扩展所构成的一种建模语言.受控对象被抽象成混成自动机HA, 其定义如下所述.

定义3.混成自动机为多元组HA=$(\tilde x, {\tilde x_0}, V, {v_0}, inv, dif, E, act, lab, syn), $其中各元素的含义如下.

$\tilde x = ({x_1}, {x_2}, {x_3}, {x_n}) \in {\mathbb{R}^n}$是实数值连续状态变量的有限集合.

${\tilde x_0}$是连续变量初始条件.

V是离散状态 (位置节点) 的有限集合.

${v_0} \in V$是初始位置的集合.

inv是一个标注函数, 它为每个位置v∈V赋予一个关于$\tilde x$的不变集约束inv(v).

dif是一个标注函数, 它为每个位置赋予一个关于$\tilde x$的微分方程.

E∈V×V是所有离散变迁 (或边) 的有限集合.

$act = \{ act(e)|e \in E\} $是一个将E中的转换e标注为一组约束的标注函数, 它为每条边e∈E赋予一个能触发离散变迁的连续变量取值条件.

lab是一组同步标记的集合.

syn是一个将E中的转换e标注为一组同步约束的标注函数.

图 4为TableSat受控对象的混成自动机模型 (TableSat介绍详见第6.2节), 其中连续变量ω表示转盘角速度, ν表示风扇转速, t表示时间, 离散位置On_AD, On_DA, On_Rest表示在风扇电压处于“12V”状态下, 转盘分别处于采样、计算控制和控制后状态.离散位置Off_AD, Off_DA, Off_Rest表示在风扇电压处于“0V”状态下, 转盘分别处于采样、计算控制和控制后状态.假设起始转盘角速度, 风扇转速, 开始时刻都为0, 风扇电压处于“12V”状态.当风扇电压处于“0V”时, 转盘角速度ω随微分方程变化而下降; 当控制指令On到达时, 风扇电压将由“0V”状态转变为“12V”状态, 系统则变迁至On模式开始加速; 此时, 若风扇电压处于“12V”, 则转盘角速度ω随微分方程变化而上升; 若控制指令Off到达, 则风扇电压将由“12V”状态转变为“0V”状态, 系统变迁至Off模式又开始减速.

由于混成自动机中连续行为非常复杂, 现有的相关工具大都使用多面体计算来判定线性混成自动机状态空间的可达集, 复杂度高、效率低, 无法解决实际应用规模的问题.因此, 本文的研究主要关注于其中一个比较特别的子类——线性混成自动机.线性混成自动机的流条件一般分两类.一类形如$\dot x \in [a, b]$的自动机形式, 相应的流条件积分展开后可以得到变量x的取值是与时间t相关的线性函数.另一类形如$\dot x = Ax(t) + Bu(t), $其积分展开后会成为包含e^t的非线性方程.第1类可以精确求解, 第2类形式主要依靠数值解法来解决, 把连续性的问题加以离散化, 采用“步进式”求出离散节点的数值解, 即

$ \dot x = Ax(t) + Bu(t) \Rightarrow x[k + 1] = {A_d}x[k] + {B_d}u[k]. $

数值解法会引入误差, 以经典四阶龙格库塔法 (Runge-Kutta) 为例, RK4法是四阶方法, 也就是说, 每步的误差是h⁵阶, 而总积累误差为h⁴阶.要提高精度需要根据问题选择合适的数值算法.

下面给出协同验证模型的统一形式描述, 并建立模型描述的层间关系.

定义4(标记迁移系统).一个标记迁移系统TS是一个四元组$TS = (States, Labels, \to, {S_0}), $其中, States是一个状态的集合, Lables是一个标记的集合, $\to :States \times Labels \times States$状态转换的集合, ${S_0} \in States$是初始状态的集合.

定义5.一个系统统一验证模型的形式描述表示为HAPS=LPDS||HA, 表示系统组合同步后的乘积自动机.

HAPS将各成员依据共享事件标签进行笛卡尔乘积, 构造出系统组合同步后的乘积自动机.因此, 针对LPDS每条变迁, 都要搜索HA的所有变迁去构建HAPS的变迁规则, 即需要在LPDS模型每条变迁的后面插装HA模型.HAPS的语义可以定义为一个状态迁移系统.HAPS的状态迁移也分为连续迁移和离散迁移两种类型, 其中离散迁移又分为两类:一类是HAPS中的子自动机独立地执行其内部迁移而引发的HAPS的状态迁移; 另一类是HAPS中的两个子自动机之间通过同步标记进行同步, 然后这两个子自动机执行其内部迁移而引发的HAPS的状态迁移.

首先定义同步标记和同步标注函数.

(1) 带标记的下推系统LPDS的输入字母表I是定义在混成自动机HA离散状态上的原子命题的集合的幂集;

(2) 混成自动机HA的同步标记lab是定义在带标记的下推系统LPDS状态上的原子命题的集合的幂集;

(3) 两个同步标注函数:

${L_{P2H}}:(G \times \mathit{\Gamma } ) \to lab, $在LPDS的每个配置赋予一组命题集合, 以TableSat为例, 图 2中L_P2H的赋值情况为${L_{P2H}}({\diamondsuit _3}, dscDAConver{t_0}) \to da, $程序其余状态都为${L_{P2H}}({\diamondsuit _0}, mai{n_2}) \to no\_evt.$

${L_{H2P}}:V \to I, $在HA的每个离散状态赋予一组命题集合, 以TableSat为例, 图 4中的L_H2P的赋值情况为${L_{H2P}}(On\_{\text{AD}}) \to ad, $${L_{H2P}}({\text{Off}}\_{\text{AD}}) \to ad, $其余离散状态都为${L_{H2P}}(xx) \to no\_event.$

定义6.系统统一验证模型 (HAPS) 的状态是$s = (g, \omega, v, \tilde x), $其中, g是LPDS的状态, ω是LPDS的栈字母表, ${\tilde x_0}$是连续变量初始条件, V是HA的离散状态.

假设有一个标记迁移系统S, 其初始状态为S₀.一个以S₀为根的系统行为轨迹是一个有限的或者无限的序列, 其路径是

$ t = init({s_0}) \wedge {\Delta _{p'}}({s_0}, {s_1}) \wedge {\Delta _{p'}}({s_1}, {s_2}) \wedge ... \wedge {\Delta _{p'}}({s_{k-1}}, {s_k}) \wedge ..., $

k步的路径为

$ {\left[{HAPS} \right]^k} = init({s_0}) \wedge {\Delta _{p'}}({s_0}, {s_1}) \wedge {\Delta _{p'}}({s_1}, {s_2}) \wedge ... \wedge {\Delta _{p'}}({s_{k -1}}, {s_k}). $

不确定因素.系统在运行过程中通常会有不确定因素, 如应用程序向作动器写入控制指令, 在第1.2节的分析中, 由于操作系统优先级抢占的调度策略和控制器计算执行时间的不定使得输入/输出的延迟J_io可能会不同, 因此控制指令的输出时刻并不确定.通常情况下, 我们希望系统能够描述在一定范围内的所有可能输出时刻.因此, 在可达性的分析过程中, 我们将这些不确定因素通过不确定函数non-determinism来描述, 并将不确定量定义在一个固定集合中, 如${J_{io}} \in [m, n] = \{ r \in \mathbb{R}|m \leqslant r \leqslant n\} (m, n \in \mathbb{R})$用于对控制应用程序或物理模型的时钟变量做约束, 在程序中表示为{float non_determinism (); J_io=non_determinism (); __CPROVER_assume ((n < =J_io) & & (J_io < = m)); }.

4 系统验证算法

根据混成自动机网络的操作语义, 网络中的各自动机既可以并发执行各自的动作, 又可以在共享事件标签上实现同步通信.然而, 依据此方法所生成的组合自动机的规模随着成员数目的增长而急剧增加, 从而影响了可验证系统的规模, 而这也正是著名的组合状态空间爆炸问题.为了应对该问题, 一是利用偏序规约化简组合自动机的迁移关系; 二是将形式化验证技术和协同仿真技术结合起来, 通过仿真观察记录系统的运行, 并利用仿真的运行记录对某些重要节点状态进行形式化验证.

4.1 可达性

有界模型检验方法的基本思想是有限步的展开程序控制流程图, 检查在该步数内能否找到错误状态, 若找到, 则返回系统不安全的信息, 若找不到, 则增加步数, 直到步数到达上界, 此时返回找不到错误状态的信息.

(1) 可达性, 即Fφ.我们用下面的式子表达系统模型是否在k步内可达.

$ {\left[{M \vDash \mathcal{F}\varphi } \right]^k} = init({s_0}) \wedge \Delta ({s_0}, {s_1}) \wedge ... \wedge \Delta ({s_{k -1}}, {s_k}) \wedge \bigcup\limits_{i = 0}^k {\varphi ({s_i})} . $

通过将系统验证模型转换为下推系统PDS, 那么验证模型的可达性问题可被转换为PDS的可达性分析, 然后就可以使用PDS的模型检验工具进行验证.通过转换得到的PD=$(G, \mathit{\Gamma }, \Delta, {c_0}), $其中, $G = V \times G' \times \tilde x, $ ${c_0} = \left\langle {\left( {{v_0}, {g_0}} \right), {{\tilde x}_0}, {\omega _0}} \right\rangle, $V是定义为整数型的离散状态, G'是程序状态的有限集合, $\tilde x$是定义为浮点类型的实数集, Γ是程序堆栈字母表的有限集合, Δ将各成员自动机依据共享事件标签进行笛卡尔乘积所产生的变迁条件.

一个程序的状态可以表达为$s = \langle g, \omega \rangle, $其中, g∈G是为程序状态的有限集合, w∈Γ是程序栈字母表的有限集合.可达集合是在程序的指定位置, 并且变量满足一定的约束.这里的约束是一个谓词表达式, 例如x=12∧y > 13.4, 也就是所有的变量值满足x=12∧y > 13.4.在程序的指定位置插入断言assert (x=12∧y > 13.4), 就表达了一个状态集合.基于断言的属性规约描述了从程序的初始状态到某个状态集合的可达性.通常情况下, 这个断言是一个否定形式的表示, 那么当一个满足公式的赋值被SAT/SMT找到之后, 这个赋值对应的路径就是一个违反需要验证的性质的反例.

4.2 LTL模型检验算法及优化

1.模型检验算法

1) 安全性转化为可达性分析

可达性问题与安全性问题的关系在于, 将系统不安全的行为构建成一个独立的离散状态, 然后检验此状态是否可达:如可达, 则系统中可能发生不安全行为; 反之, 则系统行为安全.因此, 检验系统安全性的问题就变成了计算系统可达空间的问题.

2) 活性转化为基于四值语义的LTL检测

系统模型是M, 系统的属性φ是用LTL描述, 我们的目的是通过有界模型检验M是否满足LTL描述的规约φ.如果把φ看成某类自动机, 模型检验问题就是判断M的语言是否包含在φ的语言, 即L(M)⊆L(φ).时序逻辑LTL的活性验证难点在于:

(1) 考虑研究如何把LTL时序逻辑公式表示的性质分解为与其等价的一组断言, 插装到程序的适当位置, 根据断言的违反情况即可判断出性质的满足情况.

(2) 运行时验证既要考虑可终止的程序, 也要考虑类似反应式系统这样的非终止程序, 此时在任何时刻只能获得当前执行的一个有穷状态前缀, 需要对时序逻辑的语义进行适当的修改, 变为针对有穷路径, 同时与基于无穷路径的时序逻辑公式语义相一致.

Büchi自动机 (Büchi automata, 简称BA) 的定义如下.

定义7. Büchi自动机是具有如下形式的五元组$\left( {\mathit{Σ} ,Q,\delta ,{q_0},F} \right),$其中各元素的含义如下.

Σ 是输入字母表的有限集合.

Q是状态的有限集合.

Δ:$\delta \subseteq (Q \times \Sigma \times Q)$是状态转换的集合.

q₀: q₀∈Q是初始状态.

F: F⊆Q是终止状态集合.

LTL检测的基本思想是做Büchi自动机的判空运算.因此, LTL检测算法包括3步.

1) 给定系统性质描述的LTL公式φ, 并利用LTL2BA工具^[26]构造相应的广义Büchi自动机${A_{\neg \varphi }}.$

目前, C程序广泛应用在嵌入式系统开发中, 其语义被工程师广泛理解, 因此我们把BA转换成等价的用C程序描述的一组断言.如图 5所示.对于公式φ=G(p→Fq), 首先对公式φ取反, 即¬φ.图 5左边是¬φ所对应的${\text{B}}{{\text{A}}_{\neg \varphi }}, $右边是等价的用C程序描述的一组断言.自动机是独立于程序本身的, 因此与程序分离不会影响程序自身的结构.在嵌入式多事件系统中, 该方法将有利于对系统属性规约.如图 3~图 4所示, 每次执行monitor函数时, 通过__CPROVER_assume () 语句使得每当${\text{B}}{{\text{A}}_{\neg \varphi }}$迁移条件满足时才能进入其后的语句, 即记录当前状态.当程序要终止时, 再根据statevar状态值和程序的状态, 依据判定准则进行判断.

2) 利用同步积算法求出积自动机$B = HAPS \times {A_{\neg \varphi }}.$系统模型每发生一次转移, 由LTL转化为的Büchi自动机也要发生一次转移.这就需要将LTL时序逻辑公式插装到在系统验证模型等价的C程序里的每条语句后.

3) 程序运行时, 验证器检测判定L(B) 是否为空, 如为空, 则说明构建的HAPS模型满足性质; 否则, 不为空的接收集即是违背性质的反例.

生成接收有穷序列的自动机 (验证器), 该自动机接收当前执行的有穷前缀, 输出相应的验证结果, 使得在存在软件缺陷的情况下尽可能早地检测到该缺陷.基于以往执行轨迹 (有穷前缀) 的记录, 能够根据基于四值语义检测系统缺陷和异常, 及早终止对程序的进一步检测.基于四值语义的LTL的判定准则.

(1) ${{\left[ S\vDash \varphi \right]}_{B}}=\text{Tiff}\ \nexists s\in S,\omega \in {{\Sigma }^{\omega }},{{\left[ s\omega \vDash \neg \varphi \right]}_{\omega }}=\text{T};$

(2) ${{\left[ S\vDash \varphi \right]}_{B}}\supseteq {{\text{T}}^{P}}\text{iff}\ \nexists s\in S,{{\left[ ss_{n-1}^{\omega }\vDash \neg \varphi \right]}_{\omega }}=\text{T};$

(3) ${\left[{S \models \varphi } \right]_B} = \bot {\rm{ iff }}\exists s \in S, \forall \omega \in {\Sigma ^\omega }, {\left[{s\omega \models \neg \varphi } \right]_\omega } = {\rm T};$

(4) ${\left[{S \models \varphi } \right]_B} \supseteq { \bot ^P}{\rm{ iff }}\exists s \in S, {\left[{ss_{n-1}^\omega \models \neg \varphi } \right]_\omega } = {\rm T}.$

LTL根据当前的有穷轨迹区分下面3种情况.

(1) 当前观测到的有穷轨迹u能够证明待验证的性质φ成立, 而不用考虑将来的行为.

(2) 当前观测到的有穷轨迹u能够证明无论将来发生什么行为, 待验证的性质φ始终不成立.

(3) 当前观测到的有穷轨迹u不能证明待验证的性质φ成立与否, 需要根据观测到的有穷轨迹u预测φ, 这种情况下又分两种情形.

(1) 当前观测到的有穷轨迹u不违反φ, 则φ有可能成立.

(2) 当前观测到的有穷轨迹u违反φ, 则φ有可能不成立.

2.算法的优化

系统验证模型是将各成员依据共享事件标签进行笛卡尔乘积, 因此需要在控制应用程序每条语句的后面插装受控对象模型.因此, 因为HPDS的变迁关系并不是严格意义上的笛卡尔积, LPDS和HA的各自变迁必须满足使能关系, 仅考虑离散变迁, 算法的时间复杂度O(|δ|×|Δ|).算法的优化包括对可达性分析和LTL的模型检查算优化.下面分别加以介绍.

(1) 对于可达性分析, 使用偏序规约简化

首先定义3个概念描述不同变迁条件之间的关系.

使能性 (enabledness).如果当且仅当$\tau \subseteq {L_{H2P}}(v), $则称一个LPDS的变迁关系$r = \left\langle {g, \gamma } \right\rangle \mathop \to \limits^\tau \left\langle {g', \omega } \right\rangle \in \Delta $在一个HA离散状态V使能, 否则, γ被V否定发生变迁.同样地, 对于一个HA的离散变迁$d = \left\langle {v, \tilde x} \right\rangle \mathop \to \limits^\alpha \left\langle {v', \tilde x'} \right\rangle $能够被一个LPDS的配置〈g, γ〉使能发生变迁当且仅当$\alpha \subseteq {L_{P2H}}(g, \gamma ), $否则, d被〈g, γ〉否定发生变迁.

例如一个LPDS的变迁关系$\left\langle {{\diamondsuit _1}, reanSensor{s_0}} \right\rangle \xrightarrow{{ad}}\left\langle {{\diamondsuit _1}, dscADSca{n_0}reanSensor{s_1}} \right\rangle $(图 2中第19条语句) 和一个HA离散状态On_AD (如图 4所示), L_H2P(On-AD)→ad, 则离散状态On_AD使变迁$\left\langle {{\diamondsuit _1}, reanSensor{s_0}} \right\rangle \xrightarrow{{ad}}$ $\left\langle {{\diamondsuit _1}, dscADSca{n_0}reanSensor{s_1}} \right\rangle $能够发生.但是对于HA离散状态On_DA, 因为L_H2P(On-DA)→no_vert, 所以离散状态On_DA使变迁$\left\langle {{\diamondsuit _1}, reanSensor{s_0}} \right\rangle \xrightarrow{{ad}}\left\langle {{\diamondsuit _1}, dscADSca{n_0}reanSensor{s_1}} \right\rangle $不能发生.

不可分辨性 (indistinguishability).给一个HA的离散变迁$d = \left\langle {v, x} \right\rangle \mathop \to \limits^\alpha \left\langle {v', \tilde x'} \right\rangle (e = (v, v'), \tilde x \mapsto act(e)), $一个LPDS的变迁关系$r = \left\langle {g, \gamma } \right\rangle \mathop \to \limits^\tau \left\langle {g', \omega } \right\rangle \in \Delta $对d是不可分辨的当且仅当$\alpha \subseteq {L_{P2H}}(g, \gamma ) \cap {L_{P2H}}(g', \omega ).$同样地, d对于γ是不可分辨的当且仅当$\tau \subseteq {L_{H2P}}(v) \cap {L_{H2P}}(v').$

例如对于一个HA的离散变迁${t_2} = {\text{On}}\_{\text{DA}}\xrightarrow{{\{ t > {t_o} \cap {\text{On}}\} }}{\text{On}}\_{\text{Rest}}$(如图 4所示), 一个LPDS的变迁关系$\left\langle {{\diamondsuit _0}, mai{n_2}} \right\rangle \xrightarrow{{no\_evt}}\left\langle {{\diamondsuit _0}, wait\_cloc{k_0}mai{n_3}} \right\rangle $(如图 2中第4条语句所示), 由于${\text{On}} \subseteq {L_{P2H}}({\diamondsuit _0}, mai{n_2}) \cap {L_{P2H}}$ $({\diamondsuit _0}, wait\_cloc{k_0}mai{n_3}), $所以该LPDS的变迁关系对t₂是不可分辨的.但是对于另一个LPDS的变迁关系$\left\langle {{\diamondsuit _3}, } \right.$ $\left. {commandMotor} \right\rangle \xrightarrow{{da}}\left\langle {{\diamondsuit _3}, dscDAConver{t_0}commandMoto{r_1}} \right\rangle $(见图 2中第24条语句), 由于${L_{P2H}}({\diamondsuit _3}, dscDAConver{t_0}) \cap $ ${L_{P2H}}({\diamondsuit _3}, dscDAConver{t_0}commandMoto{r_1}) = \emptyset, $所以该LPDS的变迁关系对t₂是可分辨的.

独立性 (Independence).给一个HA的离散变迁d和一个LPDS的变迁关系γ, 如果d和γ相互不可分辨, 我们就说d和γ相互独立; 否则, d或者γ不是不可分辨并且d和γ满足使能关系, 我们就说d和γ是相互依赖的.独立性是对称的.

例如对于一个HA的离散变迁${t_1} = {\text{On}}\_{\text{AD}}\xrightarrow{{\{ t > {t_i}\} }}{\text{On}}\_{\text{DA}}$(如图 4所示) 和一个LPDS的变迁关系$\left\langle {{\diamondsuit _0}, mai{n_2}} \right\rangle \xrightarrow{{no\_evt}}\left\langle {{\diamondsuit _0}, wait\_cloc{k_0}mai{n_3}} \right\rangle $(图 2中第4条语句), 因为t₁和LPDS的变迁关系相互不可分辨, 所以它们相互独立.

对于一个HA的离散变迁${t_2} = {\text{On}}\_{\text{DA}}\xrightarrow{{\{ t > {t_o} \cap On\} }}{\text{On}}\_{\text{Rest}}$(如图 4所示) 和一个LPDS的变迁关系$\left\langle {{\diamondsuit _3}, commandMoto{r_0}} \right\rangle \xrightarrow{{da}}\left\langle {{\diamondsuit _3}, dscDAConver{t_0}commandMoto{r_1}} \right\rangle $(图 2中第24条语句) 不是不可分辨并且满足使能关系, 所以它们相互依赖.

可达性的优化是针对LPDS和HA的异步变迁, 如图 6所示异步变迁主要有3类变迁关系:图中的水平线代表当HA变迁, LPDS等待, 即系统验证模型的这样一类变迁关系:${\Delta _{hori}} = \left\langle {\left( {g, q} \right), \gamma } \right\rangle \to \left\langle {\left( {g, q'} \right), \gamma } \right\rangle ;$图中的垂直线代表当LPDS变迁, HA等待, 即系统验证模型的这样一类变迁关系:${\Delta _{vert}} = \left\langle {\left( {g, q} \right), \gamma } \right\rangle \to \left\langle {\left( {g', q} \right), \omega } \right\rangle ;$图中的对角线代表HA和LPDS同时变迁, 即系统验证模型的这样一类变迁关系:${\Delta _{diag}} = \left\langle {\left( {g, q} \right), \gamma } \right\rangle \to \left\langle {\left( {g', q'} \right), \omega } \right\rangle .$

经过优化, 如图 7所示化简的异步变迁主要有两类变迁关系.化简部分变迁${\Delta _{hori}}:$图中的水平线代表当HA变迁, LPDS等待, 即${\Delta _{hori}} = \left\langle {\left( {g, q} \right), \gamma } \right\rangle \to \left\langle {\left( {g, q'} \right), \gamma } \right\rangle .$化简所有变迁${\Delta _{diag}}:$图中的对角线代表HA和LPDS同时变迁, 即${\Delta _{diag}} = \left\langle {\left( {g, q} \right), \gamma } \right\rangle \to \left\langle {\left( {g', q'} \right), \omega } \right\rangle .$

对比图 6和图 7可以看出, 基于偏序规约思想化简全部的${\Delta _{diag}}$和部分的${\Delta _{hori}}$并不影响系统的可达性.通过定义关键集 (sensitiveSet) 来定义哪些变迁${\Delta _{hori}}$不能被化简掉.

定义8(关键集SensitiveSet).$SensitiveSet = \left\{ {head\left( {\left\langle {{g_0},{\omega _0}} \right\rangle } \right)} \right\} \cup \left\{ {head\left( {c'} \right)\left| {\gamma {\rm{和}}d{\rm{相互依赖}}} \right.} \right\}.$

根据偏序规约, 优化后系统模型的变迁条件生产如算法1所示.算法1省去了全部${\Delta _{diag}}$和部分${\Delta _{hori}}.$因此, 仅考虑离散变迁.如图 8所示, 统一验证模型的组装只需在控制应用程序特定语句后插装受控对象模型 (函数physical_run ()).

算法1.优化后的HAPS变迁条件生成算法.

输入:${\Delta _{sync}} \leftarrow \emptyset, {\Delta _{hori}} \leftarrow \emptyset, {\Delta _{vert}} \leftarrow \emptyset .$

输出:Δ'.

Forall the $r = \left\langle {g, \gamma } \right\rangle \mathop \to \limits^\tau \left\langle {g', \omega } \right\rangle \in \Delta $ do

  Forall the$d = \left\langle {v, X} \right\rangle \mathop \to \limits^\alpha \left\langle {v', X'} \right\rangle (e = (v, v'), X \mapsto act(e)), $$\alpha \subseteq {L_{P2H}}(g, \gamma )$ and $\tau \subseteq {L_{H2P}}(v)$ do

    ifγ和d相互依赖then

      ${\Delta _{sync}} \leftarrow {\Delta _{sync}} \cup \{ \left\langle {\left( {g, q} \right), \gamma } \right\rangle \to \left\langle {\left( {g', q'} \right), \omega } \right\rangle \} $ {LPDS和HA必须同步变迁}

    else

      ${\Delta _{vert}} \leftarrow {\Delta _{vert}} \cup \{ \left\langle {\left( {g, q} \right), \gamma } \right\rangle \to \left\langle {\left( {g', q} \right), \omega } \right\rangle \} $ {LPDS变迁, HA等待}

    if$\left\langle {g, \gamma } \right\rangle \in SensitiveSet$ then

        ${\Delta _{hori}} \leftarrow {\Delta _{hori}} \cup \{ \left\langle {\left( {g, q} \right), \gamma } \right\rangle \to \left\langle {\left( {g, q'} \right), \gamma } \right\rangle \} ${HA变迁, LPDS等待} $\Delta ' \leftarrow {\Delta _{sync}} \cup {\Delta _{hori}} \cup {\Delta _{vert}}$

以TableSat为例, 将图 4表示的混成自动机转化等价的C程序.转换后的C程序如图 9所示.第1行定义了3个浮点类型变量physical, nu和t, 分别表示3个连续变量$(\omega, v, t);$第2行, 函数physcial_dynamic1描述了HA模型的连续行为, 即物理运动方程; 第5行~第30行实现了TableSat的行为变迁, 每次执行函数physical_run, 都会通过system_mode (第5行和第22行) 判断HA模型所处的状态:是处于12V的还是处于0V的状态; 第6行、第13行和第17行, 判断变量t是否满足act(e); 第10行、第16行和第20行通过调用函数physcial_dynamic1在一段时间内运行HA模型; 第7行和第8行通过将时间t设为符号量, 并假设限定在区间[t_s, t_i), 第14行和第15行、第18行和第19行类似.

另外, 由于使用了偏序规约优化, 化简掉了部分系统的下一状态, 所以LTL属性规约中不包括X算子.

(2) 对于活性

线性时序逻辑 (LTL) 对模型属性进行规约, 模型每发生一次转移, 由LTL转化为的Büchi自动机也要发生一次迁移.根据第3.5.3节的算法, 在将LTL时序逻辑公式自动转换为与其等价的一组断言后, 我们需要将一组断言插装到在HAPS等价的C程序里的每条语句后, 这样会造成验证规模的极大增加, 因此, 需要针对活性验证算法进行化简.如果当一条HAPS的变迁并不改变φ中命题变元的值时, 此时我们不需要在这条变迁后插入这组断言去检测断言的情况, 因为该组断言变迁前后没有变化, 我们定义这种情况为该变迁关系对于LTL公式是不可见的.

定义9(可见命题).给定一个LTL公式φ和系统模型HAPS, 当且仅当${L_\varphi }(c) = {L_\varphi }(c'), $那么一个HAPS的变迁关系$t = c\mathop \to \nolimits_{{\text{HAPS}}} c'$对于φ是不可见的; 否则, t对于φ就是可见的.

${L_\varphi }(c)$表示c中的有关φ中命题变元的值, 如果${L_\varphi }(c) = {L_\varphi }(c'), $表示HAPS的变迁并没有改变φ中命题变元的值, 此时该变迁关系对于LTL公式是不可见的.

定义10(可见命题变元集合). VisProp(t) 标记了被变迁关系t所影响的命题变元集合.如果VisProp(t)=∅, t就是不可见的.

定义11(可见集VisibleSet). $VisibleSet = \{ head(\left\langle {g', \omega } \right\rangle )|\exists r = \left\langle {\left( {v, g} \right), \tilde x, \gamma } \right\rangle \mathop \to \nolimits_{{\text{HAPS}}} \left\langle {\left( {v', g'} \right), \tilde x', \omega } \right\rangle \in \Delta '对于\varphi 是可$ $见的\} .$

通过定义可见集VisibleSet, 我们只需要在程序的适当位置将一组断言插装到系统模型, 根据断言的违反情况即可判断出性质的满足情况.因此, 并不需要在将一组断言插装到系统模型每条语句后, 这极大地化简了验证规模.

4.3 综合仿真和形式化验证的协同验证

安全攸关场景的正确性在CPS系统运行安全上起着非常重要的作用.一方面, 由于CPS系统规模的不断增大, 系统的复杂性有了很大的提高, 直接对系统进行完全形式化验证已经变得越来越困难.另一方面, 虽然仿真在工程实践中已经得到了广泛的应用, 但是由于仿真测试的不完备性, 仅能在一定输入的情况下运行系统来观测系统行为, 无法穷尽地检测系统所有可能的输入与场景.因此, 结合目前工程实践中广泛应用的仿真技术, 对仿真辅助形式化验证在安全攸关系统设计中是非常必要的, 尤其是针对具有CPS特征的复杂控制应用程序.

仿真测试方法使用具体数值来表现测试场景和预期结果, 而模型检验技术使用系统模型来替代具体数值.系统模型描述了预期和非预期的系统行为.模型检验依赖严格的数学过程, 搜索系统模型的可能执行路径以获得反例.通过模型执行的形式化分析与仿真方法互补, 使用的形式化验证方法可以发现特定动态运行情况是否会发生以及在什么条件下发生.这些信息可用于改进设计以及设计需求, 用于辅助仿真调试和验证.

因此, 本文综合仿真和形式化验证方法, 提出了协同验证方法:通过仿真, 驱动系统进入某一状态, 然后结合形式化验证方法从当前仿真状态开始做k步有界模型检验.因此, 基于系统仿真, 我们可以选取系统运行过程中一个场景进行形式验证.

定义12. CPS系统行为迁移的条件记为$r = \varphi \cup t, $ φ表示事件集合, t表示时钟集合.r既可以表示为事件触发也可以表示时间触发.

因此, 一个CPS系统的路径表示${s_0}, {s_1}, {s_2}, ..., {s_{k-1}}, {s_k}, ..., {s_n}$(其中, $0 < k \leqslant n \in \mathbb{N}$), 我们将这条路径记为

$ \pi = {s_0}\mathop \to \limits^{{r_0}} {s_1}\mathop \to \limits^{{r_1}} {s_2}...\mathop \to \limits^{{r_{k-2}}} {s_{k-1}}\mathop \to \limits^{{r_{k-1}}} {s_k}...\mathop \to \limits^{{r_{n - 1}}} {s_n}. $

定义13. CPS系统行为迁移的条件序列表示为$seq = {r_0}, {r_1}, {r_2}, ..., {r_n}, n \in \mathbb{N}, se{q_i} = {r_i}$表示从第i个迁移的条件, 其中$0 \leqslant i \leqslant n.$

本文提出了一种将协同仿真和形式化验证相结合的办法, 通过仿真执行和k步有界模型检验对关键场景进行验证.首先在CPS虚拟原型中通过仿真记录一条系统执行路径π; 然后在CPS系统的状态集合$\{ {s_0}, {s_1}, {s_2}, ..., {s_{k-1}}, {s_k}, ..., {s_n}\} $中根据场景需求选择某些状态做有界模型检验.如图 10所示, 在状态${s_{k-1}}$上, 结合迁移的条件$se{q_{k-2}}$共执行了4步模型检验, 其中, ${S'_{k, 1}}$表示执行第1步模型检验时系统所处的状态.将${s_{k-1}}$作为关键状态, 则在状态${s_{k-1}}$上, 结合迁移的条件$se{q_{k-1}}$共执行了4步模型检验, 其中, ${s'_{k, 1}}, {s'_{k, 2}}, {s'_{k, 3}}$和${s'_{k, 4}}$表示执行第1步、第2步、第3步和第4步模型检验时系统所处的状态.

5 协同验证工具原型

如图 11所示, 我们实现了LTL模型检验算法.协同验证工具原型Co-Ver基于CBMC.CBMC是一个针对C程序的模型检查器, 它擅长检查程序的诸如检查数组边界、缓存溢出、指针安全等程序性质.

协同验证工具接受3类输入:(1) LTL规约; (2) 控制应用C程序; (3) 受控对象模型.验证主要有4个步骤:

(1) 通过LTL2BA工具将LTL规约转换成BA, 然后再将BA转换为相应的C程序所描述的一组断言^[26].

(2) 将受控对象 (HA模型) 转换为相应的C程序, 然后与控制应用程序 (LPDS模型) 组装成统一验证模型HAPS (C程序描述).

(3) 将规约插装到模型HAPS的适当位置.

(4) 执行有界模型检验.

通过不确定函数non-determinism () 描述系统中的不确定行为, 如采样的延迟.通过假设assume来限制系统可能造成的非确定性, 并用断言assert将要验证的属性的声明添加到设计的内部状态之中.因此, 结合假设assume、断言assert和不确定函数non-determinism () 可以构造丰富的场景.

使用模型检验可以是对仿真的一个补充, 它能够将仿真结果用于形式化方法进行模型分析.传统仿真测试方法使用具体数值来表现测试场景和预期结果, 而模型检验技术使用系统行为模型来替代具体数值.系统行为模型可以包括模型测试方案和验证目标, 描述预期和非预期的系统行为.通过行为模型执行的形式化分析与仿真方法互补, 使用的形式化方法可以发现特定动态运行情况是否会发生以及在什么条件下发生.这些信息可用于改进设计以及设计需求, 用于辅助仿真调试和验证.协同仿真和模型检验综合验证框架如图 12所示.

本文提出了针对实现层的CPS协同验证技术方法.基于所设计的虚拟执行平台Co-Sim^[27]对嵌入式系统进行协同仿真:使用QEMU和Matlab模拟仿真物理实体连续动态变化、计算实体离散动态变化及其运行时交互过程.首先通过协同仿真, 在虚拟执行环境中执行测试用例并记录系统信息, 然后将仿真数据导出成系统的状态序列, 最后在形式化验证工具中执行模型验证并输出验证结果.其中, 执行框架Execution harness是一个包含了系统验证模型和仿真数据 (这些数据已经过配置) 的集合, 用以验证一个系统, 使其在不同的条件下运行, 并监控其行为和输出.执行框架有3个主要的组成部分:执行引擎、模型和仿真数据库 (repository).验证如算法2所示.

算法2.混合执行路径验证算法.

输入:仿真路径集${s_n} \in ST, $待验证状态集$ws \in WS, $控制周期T, A/D转换完成时刻$t_i^k, $D/A转换完成时刻$t_o^k, $截止时间Time_Bound.

输出:验证结果Result.

Forall the i < num do

  i←0;  //loop iteration

  ${s_n} \leftarrow Load\_Simulation\_Trace(ST);$

  $num \leftarrow number\_of\_state\_in\_ws;$

  ${s_i} \leftarrow Get\_State(ws, i);$

  ${s_{i, 0}} \leftarrow Reset\_State({s_i});$

  while $t < Time\_Bound$ do

    ${s_{i, k + 1}} \leftarrow Compute\_Next\_state({s_{i, k}});$

    $\operatorname{Re} sult \leftarrow Check\_State({s_{i, k + 1}})$

    $k \leftarrow k + 1;$

end while

end for

6 实验结果与分析

为了验证本文所提出的方法, 我们做了两组实验:一是混成系统的经典例子——温控自动控制系统; 二是一个实际的嵌入式自动控制系统TableSat.实验平台:3.40GHz Intel (R) Core (TM), 16G memory, Ubuntu 12.04 64位操作系统.

6.1 温度自动控制系统

温度自动控制系统:利用控制器保证某一特定空间温度达到期望值的系统, 是一个经典的混成系统案例, 我们通过改造成为一个嵌入式控制系统应用场景.在温控系统中, 环境温度是连续变化的物理过程, 温控器是离散的计算过程:当控制器检测到系统温度降低到19℃以下时, 控制应用就发出控制指令on, 从而打开加热器, 对系统进行加热; 而当系统温度高于21℃时, 则正好相反, 控制应用发出控制指令off, 从而关闭加热器.温度自动控制系统要确保环境温度在18℃~22℃之间.

1) 系统属性

首先使用LTL描述系统属性, 然后通过工具形成相应的C程序段.

规则1.控制器永远不会将温度加热超过一个上限, LTL形式化表示为G$(Temper \leqslant TemperUpLimit).$

规则2.温度不会低于一个下限, LTL形式化表示为G$(Temper \geqslant TemperDownLimit).$

规则3.当温度超过上界值时, 控制器总会发出off指令, LTL形式化表示为G($(Temper \geqslant up\_th) \to $F(Off).

规则4.当温度低于下界值时, 控制器总会发出On指令, LTL形式化表示为G($(Temper < down\_th) \to $F(On).

然后将描述LTL的C程序段插装到程序的适当位置, 执行有界模型检验.

2) 形式化验证

(1) 目前的验证方法一般不对控制周期进行细分, 尤其是控制领域, 通常假设计算不消耗时间, 即在采样、计算和控制是在同一时刻完成, 因此第1个实验场景也基于这个思想设置.实验参数:温度初始值不确定, 是范围在^{[19, 24]}之间的实数值; 温控器处于关闭状态; 系统的控制时间间隔t=0.3s, A/D转换完成的时刻t_i=0.0s, D/A转换完成的时刻t_o=0.0s, 即从A/D转换到D/A转换的时间间隔为 (d=0s).

图 13是受控对象温度在这个场景下的模型图.在该模型中, 连续变量t表示时间, 连续变量x描述的是系统中实时变化的温度数值.离散位置On_AD, On_DA表示加热器被打开 (on) 时, 环境温度分别处于采样和计算控制状态.离散位置Off_AD, Off_DA表示在加热器被关闭 (off) 时, 环境温度分别处于采样和计算控制状态.当控制指令Off到达时, 加热器被关闭, 环境中的温度按照物理规律$\dot x =-2$下降; 当控制指令On到达时时, 加热器被打开, 环境中的温度按照物理规律$\dot x = 4$上升.系统的初始条件被设定为温度20℃.

然后针对这个场景对系统属性1~属性4执行有界模型检验, 实验结果见表 1.

实验结果显示, 只有规则1不满足, 其余规则都满足.规则1不满足的原因在于, 当时环境温度接近上限 (22℃) 时, 温控器仍然打开加热器, 使得环境温度达到22.031 76℃, 超过了上界.另外, 有界模型检测的效率与循环和递归的展开有密切的关系, 因为 (1) 循环和递归展开会使代码量激增; (2) 代码的增加会导致变量复制的增加.通过实验结果分析, 验证的时间开销主要来自于求解器, 当控制循环次数达到150时, 验证需要2 015.53s.

(2) 为了与第1个实验作对比, 我们做了第2个实验.在第2个实验中考虑了采样控制时间的影响:系统的控制时间间隔T=0.3s, A/D转换完成的时刻t_i=0.0s, D/A转换完成的时刻t_o=0.2s, 即从A/D转换到D/A转换的时间间隔为 (d=0.2s), 由于采样延迟抖动 (j_s∈[0, 0.1]) 和输入/输出抖动 (j_io∈[0, 0.05]) 不确定, 利用不确定函数non-determinism () 设置为符号量.其他实验参数:温度初始值为20, 温控器处于关闭状态.图 14是受控对象温度在这个场景下的模型图.图 14与图 13所描述的模型类似, 增加了两个离散位置On_Rest和Off_Rest, 分别表示加热器被打开 (on) 时和关闭 (off) 时的控制后状态.系统的初始条件被设定为温度20℃.

然后针对这个场景对系统属性1~属性4执行有界模型检验, 实验结果见表 2.实验结果显示, 所有规则都满足.规则1在第2个实验中满足的原因在于, 当环境温度接近上限时, 在控制时刻上温控器会更早关闭加热器.通过细致分析可以发现, 第2个实验场景更符合实际情况, 计算不消耗时间的假设过于理想.另外, 在本实验中对比了算法优化的效果, 本例中的Timeout时间设为3 600s.通过实验结果可以清楚地看出, 算法的优化效果很明显, 时间开销平均降低了82%.

6.2 TableSat

人造卫星姿态控制模拟环境TableSat, 如图 15所示, 是一个模拟卫星姿态控制的自由度实验平台.NASA使用这套实验平台模拟人造卫星姿态的变化、采样和控制过程.我们通过与University of Michigan的合作在实验室搭建了这套实验平台.本文将主要通过TableSat作为人造卫星姿态控制应用场景的实验平台.

TableSat模拟了卫星的姿态控制过程.PC/104通过16位的模拟数字转换器获得角速度传感器所测的转盘角速度值, 根据控制算法计算所应施加的给电脑风扇的电压值, 然后通过16位的数字模拟转换器完成电脑风扇电压的控制, 并且通过802.11b无线接口与实验机 (模拟地面卫星接收站, ground station) 通信.用户设计实现转盘角速度的控制算法用来控制转盘的转速, 使得转盘的转速维持在预定目标值.TableSat在运行期间, 实时并发计算、环境感知以及自主控制依据严格的时间约束在持续地融合, 并与物理环境不断交互, 共同确定下一时刻的行为.

在人造卫星控制问题中, 从简单的姿态控制到复杂的交会问题, 大多数情况都采用燃料燃烧所产生的推力或力矩进行控制, 为了节省昂贵的燃料, 工程上提出燃耗最少的控制问题.单纯以节省燃料为目的的控制往往导致系统的响应过慢, 因而又出现了兼顾响应时间及燃料的时间一燃料最优控制问题.为了更好地解决以上问题, 人们提出了砰-砰 (Bang-Bang) 控制, 它是卫星系统中不可缺少的控制方式.所以本实验以一个砰-砰控制应用为例.

(1) 物理过程建模

连续系统一般会用微分方程来表示.TableSat方程线性处理后为

$ \left\{ \begin{gathered} \dot \omega = \frac{{l{K_{\omega f}}}}{I}v \hfill \\ \dot \nu =-\alpha \nu + {K_{\nu \dot \omega }}V \hfill \\ \end{gathered} \right. $

(1)

其中, I是TableSat的转动惯量, ω是TableSat的角速度, l是风扇的力臂, ${K_{\omega f}}$是风扇与动力的比例常数, u是风扇的转速, a是风扇常数, ${K_{v\dot \omega }}$是风扇电压与转速的比例常数, V是风扇所施加的电压值.

(2) 协同验证

首先使用LTL描述系统属性, 然后通过工具生成相应的C程序段.

规则1.控制器永远不会将TableSat加速超过一个速度上限, LTL形式化表示为

$ \mathit{\boldsymbol{G}}\left( {Rotary.Velocity \leqslant VelocityUpBound} \right) $

规则2.在一定时间内, 控制器必须将TableSat加速超过一个速度下限, LTL形式化表示为

$ \mathit{\boldsymbol{G}}\left( {(Time \geqslant TimeBound) \to (Rotary.Velocity \geqslant VelocityDownBound)} \right) $

规则3.当TableSat的转盘角速度超过期望值的1.5倍后, 控制器将风扇的电压置为0V, LTL形式化表示为

$ \mathit{\boldsymbol{G}}\left( {(Rotary.Velocity > 1.5 \times TargetVelocity) \to (Actuator.FanVoltage \equiv 0)} \right) $

规则4.当TableSat的转盘角速度低于期望值的0.4倍后, 控制器将风扇的电压置为12V, LTL形式化表示为

$ \mathit{\boldsymbol{G}}\left( {(Rotary.Velocity < 0.4 \times TargetVelocity) \to (Actuator.FanVoltage \equiv 12)} \right) $

规则5.在一定时间内, TableSat的转盘角速度与期望值的差的绝对值必须在误差允许范围内, LTL形式化表示为

$ \mathit{\boldsymbol{G}}\left( {(Time \geqslant TimeBound) \to (\left| {Rotary.Velocity-TargetVelocity} \right| \leqslant SteadyStateError)} \right) $

规则6.当TableSat的转盘角速度大于期望值时, 控制器总会将风扇的电压置为0V, LTL形式化表示为

$ \mathit{\boldsymbol{G}}\left( {(Rotary.Velocity > TargetVelocity) \to \mathit{\boldsymbol{F}}(Actuator.FanVoltage = fullNeg)} \right. $

规则7.当TableSat的转盘角速度小于期望值时, 控制器总会将风扇的电压置为12V, LTL形式化表示为

$ \mathit{\boldsymbol{G}}\left( {(Rotary.Velocity < TargetVelocity) \to \mathit{\boldsymbol{F}}(Actuator.FanVoltage = full)} \right. $

然后编写Bang-Bang控制器的C程序, 接着将该程序和受控对象组装成统一验证模型, 最终形成一个描述系统的完整C程序 (程序行数为644行).最后将描述LTL的C程序段插装到程序的适当位置.已知受控对象的状态方程为$\dot x = Ax(t) + Bu(t) \Rightarrow x[k + 1] = {A_d}x[k] + {B_d}u[k].$这里主要做了两组实验, 一是直接对系统进行模型检验; 二是结合协同仿真, 对关键场景辅助模型检验.下面详细加以介绍.

(1) 直接应用模型验证

从某种意义上说, 系统控制的启动瞬间响应是系统危险的时段.针对系统的初始状态不确定的情况下设计验证场景:转盘角速度初始值不确定, 是范围在[0, 40]之间的实数值; 风扇的初始电压为12V, 风扇转速为0;系统的控制时间间隔T=0.4s, A/D转换完成的时刻t_i=0.0s, D/A转换完成的时刻t_o=0.0s.角速度期望值为30deg/s, 我们将TableSat的转盘角速度初始值利用不确定函数non-determinism () 设为一定范围内的符号量ω∈[0, 40], 依据场景设定其他参数.

实验结果见表 3.在验证中, 无优化算法发现规则1违背, 路径是:当初速度为40.0deg/s, 在0.323 9197s时, 转速达到45.080 17deg/s, 此时风扇转速为13 043.52deg/s.优化后算法发现规则1违背, 路径是:当初速度为37.999 95deg/s, 在0.394s时, 转速达到45.515 26deg/s, 此时风扇转速为13 463.87deg/s.

通过实验结果分析, 验证的时间开销主要来自于求解器, 相对于温控系统, 一方面由于受控对象是一个二元二次方程组, 另一方面由于本例的规模以及大量浮点数的计算, 验证的代价比较大, 通过算法优化, 验证的耗时显著提高.

(2) 结合仿真执行模型验证

在第1组实验中, 直接应用模型检验, 虽然经过优化, 可以执行有限步, 但是由于系统的复杂性, 执行的步骤有限, 所以目前无法完全直接应用模型检验.在实际的开发中, 仿真可以有效地分析系统的控制性能.通过执行典型的测试用例可以获得的仿真路径, 然后基于经验在某些容易出现问题的场景, 结合仿真的数据作为初态, 用模型检验辅助验证场景.

仿真测试场景:在时间段[0s, 40s) 时, 控制目标值为30deg/s; 在时间段[40s, 80s) 时, 控制目标值为50deg/s; 在时间段[80s, 120s) 时, 控制目标值为70deg/s; 在时间段[120s, 160s) 时, 控制目标值为20deg/s; 在时间段[160s, 200s) 时, 控制目标值为50deg/s; 在时间段[200s, 240s) 时, 控制目标值为30deg/s.测试采用固定周期 (T=0.4s), A/D转换完成时刻为 ($t_i^k \in \left[{0, 0.1} \right]$), D/A转换完成时刻为 ($t_o^k \in \left[{0, 0.1} \right]$).我们每0.01s记录一次测量值, 仿真结果如图 16所示.

在仿真中, 延迟是由某个区间上的随机函数产生, 在每次仿真中是某一常值, 因此测试是不完备的.在系统初始状态为0时, 当系统采样抖动J_s和输入/输出j_io不确定的情况下, 测试控制器能否正确地控制受控对象.结合仿真数据, 我们将7条系统性质应用于模型验证中, 在这条仿真路径上共选取了8个状态点, 在每个状态点执行3步.下面主要介绍其中两个场景的实验.

场景1.当系统阶跃响应曲线第1次越过稳态值而达到峰点时记录到达峰点时刻系统的状态, 然后基于这一状态执行有界模型检验.由于系统中部件具有惯性, 故系统在外作用下由一个平衡状态 (或稳态) 过渡到另一个平衡状态 (或稳态) 需要有一个过程, 这一过程称为瞬态过程.在瞬态过程中, 系统阶跃响应曲线第1次越过稳态值而达到峰点时, 系统的采样抖动J_s和输入/输出j_io不确定的情况下, 测试控制器能否正确地控制受控对象.

根据仿真数据, 在t=3.5s时刻, 系统阶跃响应曲线第1次越过稳态值而达到峰点 (w=36.7298deg/s), 记录此时系统的状态.将采样延迟抖动 (j_s∈[0, 0.1]) 和输入/输出抖动 (j_io∈[0, 0.1]) 利用不确定函数non-determinism () 设为符号量.实验结果见表 4.

场景2.当控制目标值从20deg/s切换到50deg/s时, 系统的采样抖动J_s和输入/输出j_io不确定的情况下, 测试控制器能否正确地控制受控对象.根据仿真数据, 在t=160s时刻, ω=25.0607deg/s, 风扇转速:1788.54, 记录此时系统的状态.将采样延迟抖动 (j_s∈[0, 0.1]) 和输入/输出抖动 (j_io∈[0, 0.1]) 利用不确定函数non-determinism () 设为符号量.实验结果见表 5.

从上述的实验结果可以看出, 随着系统规模的不断增大, 直接对实现级CPS系统进行形式化验证已经变得越来越困难.在本例中, 如果直接对TableSat进行模型检验, 时间开销很大, 基本只能检查系统从初始开始3步内的行为.但是结合仿真, 我们可以在整条仿真路径上对某些关键场景辅助模型检验, 在该实验中, 每个场景能够检查3步内的行为, 总计可以检查8个关键场景共24步状态空间的行为.可以利用Co-Sim对不同的场景以及场景转换的组合情况进行仿真, 然后再将仿真结果用形式化方法进行验证.Co-ver提供了LTL属性模型检验, 在指定的时间内, Co-ver会验证是否存在能触发断言的情况.例如, 可以构造一些断言, 每当TableSat加速超过一个速度上限时触发.当设定的断言被违反时, 它会报错而且也会生成触发这个断言的反例.

7 结束语

与一般嵌入式系统相比, 在CPS概念兴起之后, 现在面向CPS的嵌入式系统更加强调协同, 通过实时采集环境中或者其他协作成员的数据, 从而更加智能地做出控制指令.在此类系统中, 大规模复杂异构性、延迟不确定性、精确控制以及计算过程同步或异步等需求导致非功能属性的表示和验证更加复杂.

本文基于自动机理论提出了控制环路的验证模型, 针对组合状态空间爆炸问题, 一方面在求解的过程中通过偏序规约等手段尽量化简模型规模, 另一方面结合虚拟仿真提出了综合虚拟仿真和形式化验证相结合的方法, 灵活配置验证的场景, 提高验证的可用性.针对目前属性规约描述表达能力不强, 如无法表达时序、活性等, 本文基于LTL描述属性的规约, 通过定义在物理连续变量上的布尔表达式描述物理过程, 而后将LTL性质规约公式转换为Büchi自动机, 即将性质分解为与其等价的一组断言, 然后再将这组断言插装到控制应用程序程序的适当位置, 根据断言的违反情况即可判断出性质的满足情况.运行时验证考虑控制应用这样的非终止程序, 在任何时刻只能获得当前执行的一个有穷状态前缀, 针对有穷路径基于四值语义进行判断.