2. 高可信软件国家重点实验室(华东师范大学), 上海 200062
2. National Key Laboratory of Trustworthy Software(East China Normal University), Shanghai 200062, China
MARTE(modeling and analysis of real-time and embedded system)是统一建模语言UML在实时和嵌入式方面的一个扩展, 提供了规范、设计和验证的支持, 这个新的扩展将要取代UML现有的在可调度、性能和时间上的扩展[1].在MARTE中, 时钟是访问模型时间结构的元素, 使用MARTE时间模型要定义互相依赖的时钟, 而时钟之间的这种依赖关系用专门的语言进行描述.该语言被称为CCSL(clock constraint specification language), 其定义在UML规范附录C3中[2, 3].CCSL逐渐被应用于各种实时嵌入式系统的设计, 如车载操作系统[4]以及信息物理系统[5].
CCSL中的时钟为逻辑时钟, 用于抽象地表示系统事件的发生情况, 即, 一次时钟滴答代表其对应的事件发生一次.CCSL约束可以描述系统中不同事件之间的关系, 用于限制系统的行为.所有的系统行为都应当满足预定义的约束条件, 同时还要保证这些约束条件能够保证系统不产生死锁.死锁是指在某一时刻, 所有时钟对应的事件都由于当前的时钟约束条件而无法发生.因此, 如何验证与分析CCSL约束是否满足上述条件具有理论与实际意义.
作为一个新兴的建模语言, CCSL吸引了许多研究人员寻找对CCSL约束进行形式化分析的有效方法, 如可调度性、死锁检测(deadlock detection).Frederic等人在其文献[6]中详细讨论了已有的关于CCSL的分析方法, 主要方法包括利用状态迁移系统[6]、Promela语言[7]、Büchi自动机[8]、时间自动机[9]、重写逻辑[10]等对CCSL约束进行转化.然而, 这些转换方法都存在一定的缺陷.例如, 基于状态迁移系统或自动机的方法如文献[7-9]中方法只能应用于对无状态的约束关系的建模, 无状态约束关系是指其时钟的当前行为与其之前的行为无关.而CCSL约束关系中的有些关系是有状态的, 如优先关系(precedence)和因果关系(causality), 因而无法利用状态迁移系统进行建模.同时, 每个约束用一个状态迁移系统表示, 这些系统合成统一的系统容易导致状态爆炸问题.另外, 这些方法需要复杂的中间变换且对集合中某个约束的修改需要对整个集合的约束进行重新转换而导致效率低下.基于重写逻辑的方法通过定义CCSL的操作语义及执行CCSL约束条件仿真所有满足这些条件的行为, 然而同样遇到状态爆炸问题.另外, 已有的这些方法也只针对某种特定的分析.
早期的工作中, 我们提出了一种基于SMT技术[12]的CCSL线性时序逻辑(LTL)模型检测方法[19].通过该方法, 将CCSL约束与LTL公式直观地转换成SMT公式, 减少了转换过程的复杂度.众所周知, SMT能够有效缓解模型检测的状态爆炸问题, 这种方法可以实现对CCSL高效的LTL模型检测(LTL model checking).然而, 模型检测依然受限于有限状态模型, 而CCSL中的调度策略是定义在整个自然数集合上的, 因此对于一些性质只能通过设定边界值验证其是部分正确的.在该工作的基础上, 本文利用SMT可满足性求解的方法证明CCSL约束之间的蕴含关系, 称之为有效性证明.有别于模型检测, 有效性证明不受状态空间的限制, 这是当前已知的大部分CCSL形式化分析方法缺少的.此外, 我们还将这种基于SMT的验证方法用于死锁检测与迹分析(trace analysis), 并将所有的功能集成到一个原型验证与分析工具.
综上, 本文的主要贡献是在原有工作[19]的基础上提出了一种基于SMT的统一的CCSL形式化分析方法, 用于有效性证明、迹分析、死锁检测及LTL模型检测, 同时开发了对应的原型验证与分析工具.具体描述如下:
(1) 提出如何利用有效性证明的方法证明CCSL约束之间的关系;
(2) 提出死锁对应的SMT公式的定义, 并利用一个具体的案例演示方法的有效性及高效性;
(3) 提出从迹(trace)到SMT公式的转化方法, 并利用具体的实例介绍转化的过程及迹分析的具体应用;
(4) 针对上述功能开发了原型验证工具, 同时支持有效性证明、迹分析、死锁检测以及LTL模型检测.
本文第1节主要介绍CCSL语法语义及其可调度性问题.第2节介绍从CCSL约束到SMT公式的转换方法.第3节分别介绍基于SMT的4种CCSL形式化分析方法的应用, 包括有效性证明、迹分析、死锁检测以及LTL模型检测.第4节介绍并展示原型工具.第5节将本文工作与相关工作进行比较.第6节总结本文并对未来工作加以展望.
1 预备知识本节主要介绍CCSL的语法语义和CCSL的可调度问题, 这些内容为CCSL约束集转换成SMT公式和基于SMT的CCSL形式化分析方法提供了理论支持.
1.1 CCSL的语法和语义我们先给出与CCSL相关的3个概念:逻辑时钟(logical clock)、调度(schedule)和历史(history)的定义[6].
定义1(逻辑时钟).逻辑时钟c是一个无穷序列
其中, ℕ+是大于0的自然数集合.如果ci的值为tick, 则表示c代表的事件在第i步时发生; 否则没发生.
定义2(调度).逻辑时钟集合C上的调度是一个函数映射δ:ℕ+→2C, 对于所有的i∈ℕ+, 都有δ(i)={c|c∈C∧ci=tick}且δ(i)≠∅.
很明显, δ(i)表示在第i步时所有活动的时钟的集合.当集合为空时称该步为空步.条件δ(i)≠∅要求每一步都至少有一个活动时钟.通过该条件, 我们只考虑每一步都至少有一个活动时钟的调度.这是因为在这样的调度中插入一些空的步并不影响时钟之间的逻辑关系, 因此只需考虑不含有任何非空步的调度即可.
定义3(历史).一个调度δ:ℕ+→2C的历史(history)也是一个函数映射χ:ℕ+→ℕ, 对于每一个c∈C和i∈ℕ+, χ定义如下:
$ \chi (c, i)=\left\{ \begin{array}{*{35}{l}} 0, &\text{ if }i=1 \\ \chi (c, i-1), &\text{ if }i>1\wedge c\notin \delta (i-1) \\ \chi (c, i-1)+1, &\text{ if }i>1\wedge c\in \delta (i-1) \\ \end{array} \right.. $ |
显然, χ(c, i)表示时钟c在到达第i步前的滴答次数.
CCSL包含12类约束的定义, 包括优先关系(Precedence)、因果关系(Causality)、从属关系(Subclock)、互斥关系(Exclusion)、并关系(Union)、交关系(Intersection)、下确界关系(Infimum)、上确界关系(Supremum)、延迟关系(Delay)、相对延迟关系(DelayFor)、周期关系(Periodicity)与取样关系(SampledOn).利用上述3个概念, 用调度满足约束的形式定义CCSL约束的语义.δ⊨ϕ表示调度δ满足CCSL约束ϕ.表 1给出了12类CCSL约束的语法和语义.
以优先关系为例, 解释CCSL约束的含义.假设有两个时钟c1与c2, 约束c1[b]≺c2表示c2可以优先比c1发生b次.当c2已经优先比c1发生b次后, c2必须等到c1发生之后才能发生.一个优先关系的应用场景是对一个初始非空队列的存取.假设队列中预先放置了b个元素, c1代表存放一个元素, c2代表取出一个元素.则c1与c2的关系可表示为c1[b]≺c2.特别地, 如果b=0, 可简写为c1pc2.关于其他约束类型的详细解释见文献[6].对于一个CCSL约束集合Φ, 用δ表示调度满足约束集Φ, 即:δ⊨Φ当且仅当∀ϕ∈Φ, δ⊨ϕ.
1.2 CCSL的可调度问题对于给定的CCSL约束集, 一个最基本的问题是判断是否存在调度满足这个约束集中的所有约束, 这便是CCSL的可调度问题.目前所知, 还没有一个算法能够对任意给定的一组CCSL约束集判断是否存在一个满足所有约束的调度.一方面是因为所求调度是无限长的, 另一方面是因为一些约束如Precedence所定义的时钟行依赖时钟的历史, 即时钟的滴答次数.若限定调度的长度, 则使问题易解.
定义4(限界调度).给定正整数n和调度δ, 如果从第1步到第n步都满足CCSL约束集Φ, 则称δ为上界为n的限界调度.
然而在实际应用中, 限界调度对于实时嵌入式系统过于限制.因为嵌入式系统的执行一般不假设时间上限, 我们期望能够求解在无限长度下满足约束条件的调度.在无限调度中存在一个特殊的情况, 即周期调度.周期调度的特点是在有限长步数后, 所有的时钟的行为都周期性发生.
定义5(周期调度).若一个调度δ中存在两个自然数l, p, 使得对任意k≥l都满足δ(k+p)=δ(k), 那么称δ为周期调度.其中, p是δ的周期.
判断周期调度的存在性目前也是一个公开问题, 其原因与判断调度的存在性一样, 关于周期调度问题的详细分析见文献[20].一个折衷的方法是, 把限界调度扩展成为周期调度.根据周期调度的定义可知:它进入周期循环之前的步数是有限的, 且周期的长度也是有限的.
定义6.给定一个上界为n的限界调度δ和两个正整数l, k, 且l < k≤n, 若δ(l)=δ(k), 那么δ可被扩展成一个周期调度δl, k:
${{\delta }_{l, k}}(i)=\left\{ \begin{array}{*{35}{l}} \delta (i), &\text{ if }i\le k \\ \delta (l+(i-l)\bmod (k-l)), &\text{ if }i>k \\ \end{array} \right..$ |
然而, 由一个满足Φ的限界调度扩展的周期调度却不一定满足Φ, 因为即使δl, k在l到k的区间内满足F, 在后续的周期循环中并不能保证满足Φ.如因果关系c1≼c2, 要保证对∀n∈ℕ+都满足χ(c2, n)≥χ(c1, n).如果在从l到k的整个区间内c1发生的次数大于c2发生的次数, 则在第k步之后的某个时刻c1滴答的累积次数将大于c2的次数.因此, 保证因果关系始终被满足的一个额外条件是在从l到k的整个区间内c2发生的次数应大于或等于c1发生的次数, 即χ(c2, k)-χ(c2, l)≥χ(c1, k)-χ(c1, l).其他的约束关系也需要类似的条件保证, 所需条件与证明可参考文献[11, 19], 在此不再赘述.此外, 像从属关系、互斥关系、并关系与交关系这类不依赖历史的约束, 因为各步之间没有关联, 则不需要额外的条件就可以保证δl, k始终满足这些约束.
2 CCSL约束集到SMT公式的转换CCSL约束集转换成SMT公式是非常直观的.给定一个时钟集合C以及在C上的CCSL约束集Φ, 为每一个时钟c∈C声明一个函数tc:ℕ+→Bool.其中, Bool表示布尔值.对于每一步n∈ℕ+, 如果tc(n)为真, 则表示时钟c在第n步滴答一次; 否则, 表示空闲.因此, 对任意n∈ℕ+, tc(n)⇔c∈δ(n)成立, 即, 一个调度δ就可由一个函数集合T={tc| c∈C}表示.再为每一个时钟c声明一个函数hc:ℕ+→ℕ, 使得对任意n∈ℕ+有下式成立:
${{h}_{c}}(n)=\left\{ \begin{array}{*{35}{l}} 0, &\text{ if }n=1 \\ {{h}_{c}}(n-1), &\text{ if }n\ge 2\wedge \neg t(n-1) \\ {{h}_{c}}(n-1)+1, &\text{ if }n\ge 2\wedge t(n-1) \\ \end{array} \right..$ |
易证明:对于任意n∈ℕ+, 都有hc(n)=χ(c, n).
根据表 1中定义的CCSL的语义, 代入hc和tc, 得到CCSL对应的SMT公式, 见表 2.对于一个CCSL约束关系ϕ, 其对应的SMT公式记为⟦ϕ⟧.另外, 根据定义1, 对每一步n∈ℕ+, δ都应满足δ(i)≠∅.该条件对应的SMT公式可定义为:∀n∈ℕ+, ∨c∈Ctc(n).
综合以上提到的tc、hc、tc与hc之间关系以及任意一个CCSL约束ϕ对应的SMT公式, 给定一个时钟集合C以及定义在C上的约束关系Φ, 则得到如下SMT公式, 记为⟦Φ⟧:
⟦Φ⟧=∧ϕ∈Φ⟦ϕ⟧∧(∀n∈ℕ+, ∨c∈Ctc(n)).
在第1.2节中提到的CCSL可调度问题, 等价于公式⟦Φ⟧的可满足性问题.根据SMT标准库SMT-LIB的定义, ⟦Φ⟧由于包含量词、未解释函数(unintepreted function)和线性整数演算(linear arithmatic), 因而属于UFLIA逻辑.而UFLIA逻辑公式的可满足性问题是不可判定的.因此, 对于某些CCSL约束集合Φ, 其对应的⟦Φ⟧的可满足性可能无法判定.
一个解决办法是, 通过设置一个边界值n消去公式中的量词.消去量词后的公式记为⟦Φ⟧n, 其可满足性问题是可判定的.一个满足⟦Φ⟧n的解即为一个上界为n的限界调度.若⟦Φ⟧n是不可满足的, 则可推出不存在一个调度满足约束集Φ, 即Φ是不可调度的.然而, 该方法无法判定Φ是否是可无限调度的.
判定Φ是否是无限可调度的不完全的方法是, 判定是否存在一个可被扩展为周期调度的限界调度.即:对于上界为n的限界调度, 判断是否存在l, k(l < k≤n), 使得∧c∈Ctc(l)⇔tc(k); 且对于Φ中某些约束, 应满足其对应的额外条件.这些额外条件向SMT公式的转化已经在前期工作[11]中做过介绍, 这里不再赘述.转化的SMT公式与⟦Φ⟧n合取公式记为
基于SMT的方法除了上述用于判断CCSL约束的可调度性之外, 对CCSL形式化分析还有更广泛的应用.本节给出了基于SMT方法的对CCSL约束形式化分析方法, 包括定理证明和模型检测.其中, 基于定理证明的方法包括有效性证明和迹分析, 基于模型检测的方法包括死锁检测和LTL模型检测.以下给出这些方法应用的具体内容, 并通过案例验证和分析其有效性与高效性.案例分析中的实验环境为Windows 10家庭版, 硬件配置为Intel® CoreTM i5-5200U处理器与4GB内存.
3.1 有效性证明(validity proving)对于CCSL的分析, 一个重要的内容是约束之间的关系, 比如优先关系蕴含因果关系, 即:如果两个时钟满足优先关系, 那么他们一定满足因果关系.相关的证明可见文献[6].更一般地, 问题可描述为给定一个CCSL约束集Φ与另一个约束ϕ, 证明任何满足Φ的调度都满足ϕ.若Φ与ϕ满足这种关系, 称Φ可推出ϕ, 记为Φ⊢ϕ.
定义7.对于一个CCSL约束集Φ和一个约束ϕ, Φ⊢ϕ成立当且仅当于每个调度δ∈Δ, δ⊨Φ ⇒ δ⊨ϕ.
其中, Δ=ℕ+×2C, C表示Φ与ϕ中所有时钟的集合.
然而, 目前证明Φ⊢ϕ成立的方法还仅限于手动证明.有些证明不仅过程繁杂, 而且再推导过程中容易犯错.
证明Φ⊢ϕ成立的问题在CCSL转化为SMT公式的基础上转化为SMT求解问题.根据第2节介绍的CSL约束集在时钟集C上的调度可以转换成一个函数集合T, δ满足Φ当且仅当T是⟦Φ⟧的一个解.同样地, δ满足ϕ当且仅当T是⟦ϕ⟧的一个解.根据定义7, Φ⊢ϕ等价于⟦Φ⟧⇒⟦ϕ⟧成立.因此, 有如下命题:
命题.对于一个CCSL约束集Φ和一个约束ϕ, Φ⊢ϕ成立当且仅当⟦Φ⟧⇒⟦ϕ⟧成立.
根据该命题, 我们知道, 证明Φ⊢ϕ成立等价于证明公式⟦Φ⟧⇒⟦ϕ⟧是永真的, 即, 它的非⟦Φ⟧∧¬⟦ϕ⟧是永假的.对于证明⟦Φ⟧∧¬⟦ϕ⟧是永假的, 现有的SMT求解器如Z3和CVC4对有些公式可直接返回结果, 对有些公式则必须通过设定一个上界n消除量词之后返回结果.对于这两种情况, 如果返回的结果为不可满足的, 则说明⟦Φ⟧∧¬⟦ϕ⟧是永假的, 即证明了Φ⊢ϕ成立.如果返回的结果是可满足的, 此时求解器会返回T的一个解, 对于第1种情况, 则说明Φ⊢ϕ不成立, 且返回的解是说明Φ⊢ϕ不成立的一种情况.对于第2种情况, 并不能证明Φ⊢ϕ是不成立的, 需要适当增加上界n的值继续求解.
表 3列出了一些通过自动定理证明的方法证明的一些性质, 证明所需要的时间以及是否需要设定上界值.首先考虑不设置上界值得情况, 如果求解器可返回结果, 则证明结束.如果在限定的时间内无法返回结果, 则设置一个边界值(默认为100)继续求解.如果在设置边界值的情况下返回的结果为可满足的, 则继续增加边界值直到结果为不满足, 或者超时.
由此可见, 通过设定边界值的证明方法是不完全的.但该方法的优势在于:通过SMT公式的转换, 借助SMT求解器的高效性实现某些定理的证明, 方法具有一定的实用性.另外, 实验结果表明:对于一些定理证明, 所需要的边界值都比较小.
3.2 迹分析迹又被称为执行迹(execution trace), 指执行路径上每一步发生的事件集合.在实时嵌入式系统中, 相应的插桩代码经过一段时间产生一个有限长度的事件序列.在CCSL中, 事件由时钟表示, 因此, 一个迹本质上是一个有界的调度.有别于定理证明与死锁检测, 因为迹是有界的, 判断一个迹是否满足对应的CCSL约束是一个可判定问题.
一段长度为n的迹可定义为上界为n的限界调度δ, 其对应的SMT公式可定义为
∧i∈(1, …, n)∧c∈Ctc(i)=v.
其中, 如果c∈δ(i), 则v表示true; 否则为false.
对于给定的CCSL约束集Φ, 验证这段迹是否满足Φ等价于验证上述公式与⟦Φ⟧n是否是同时可满足的.如果是, 则说明迹满足Φ; 否则则不满足.
以红绿闪烁灯为例, 其CCSL约束集合为{green≺red, tmp≜green$1, red≺tmp}, 表示红绿灯交替地出现.图 1表示在边界值为100时的一个迹.将迹按照上述公式转换成SMT公式并连同约束对应的公式一起验证其可满足性.求解器返回的结果为可满足.为了模拟不满足的情况情况, 对部分时钟的行为进行修改, 例如, 将时钟green在95步时改为不发生.再次对修改后的迹分析, 求解器返回的结果为不满足.
然而, 上述方法并不能显示迹在哪一步违反了约束.为了定位错误出现的位置, 将原来的公式⟦Φ⟧n修改为如下公式:
∃d∈{1, …, n}, ⟦Φ⟧d-1∧¬⟦Φ⟧d.
即:存在1~n的整数d, 使得迹在d步前都满足Φ而在d步时不满足.因此, 找出出错位置只需要用SMT求解器求解同时满足上述两个公式的d的值即可.
表 4展示了长度为200的迹进行验证的结果.实验分别对不同时钟进行不同位置的错误修改, 结果显示, 求解时间随着出错位置增大而增长.对于上述公式来说, d值增大, 因此SMT求解器需要花费更多时间.综上来说, 本小节提出的两个验证公式对于迹的分析来说都是有效的, 适用于判断迹的满足性与分析迹不满足的情况.
3.3 死锁检测
对于任何系统来说, 无死锁都是系统的基本需求.对CCSL约束而言, 所有满足约束的系统行为都被视为合法行为.因此, CCSL约束需要保证任何的合法行为都不会导致系统进入死锁状态.这里的死锁指在某个时刻没有任何一个时钟对应的事件可以发生, 每个时钟都在等待其他的时钟.
本节介绍利用SMT求解的方式检测死锁.对于给定的CCSL约束集Φ, 存在死锁等价于存在上界为某个自然数n的限界调度满足Φ, 但在n+1步时, 任何时钟产生滴答都会造成F中的某个ϕ不被满足.其对应的SMT公式如下:
$\exists n\in {{\mathbb{N}}^{+}}, {{[\![\mathit{\Phi} ]\!]}_{n}}\wedge (\forall c\in C.\forall {{t}_{c}}(n+1)\in \mathcal{B}\Rightarrow {{\vee }_{\phi \in \mathit{\Phi} }}\neg [\![\phi ]\!]_{n+1}^{n+1}), $ |
其中,
举例来检测CCSL约束集的死锁.这个例子是从AADL规范的延时分析抽象出来的实际应用组件[6], 如图 2所示.这个组件有两个输入in1和in2, 在step1和step2中分别计算, 然后在step3中计算, 最后结果由out输出.这其中不断地获取新的输入和产生结果.这个组件中的事件约束可以用CCSL描述, 图 3描绘了这些事件的9个约束.虚线箭头部分表示了两个中间事件tmp1和tmp2与其他事件的之间的约束.譬如, 我们可以得到:
tmp1≜in1+in2.
通过设置边界值n, 我们将这9个约束转换成上述的求解公式检测其可满足性.表 5展示了用Z3求解的结果, 若公式满足, 则表示存在一个死锁.否则表示不存在.另外, 我们分别用tmp1≜in1∧in2和tmp1≜in1∨in2代替tmp1≜in1+in2检测该公式的满足性.
从表中我们看到:tmp1≜in1+in2造成了死锁, 而tmp1≜in1∧in2和tmp1≜in1∨in2则没有检测到死锁.图 4表示了在用tmp1≜in1+in2关系且上界设为10时, 相关的时钟从第1步~第10步的行为及在第11步时发生死锁的情景.
在第11步时, 若in1发生, 因为tmp1≜in1+in2约束, tmp1必须发生, 从而导致tmp2也必须发生.由于out≜tmp1$1, out在此步不会发生.而tmp2与out存在优先关系约束, out要比tmp2先发生, 从而导致死锁.死锁产生的主要原因是tmp1≜in1+in2约束制约太弱, 不能保证in1和in2在out之前都要发生.而通过下确界与下确界关系约束, 则可以保证这一点, 从而避免死锁发生.效率方面, 随着界的增大, 执行时间增大, 然而都可以在较短的时间内完成检测.另外, 从表中可以看出, 无死锁的求解时间明显较短.
3.4 LTL模型检测借助SMT方法实现CCSL的LTL模型检测的主要思想是将一个LTL公式ψ, 根据既定的边界值n判断其与由CCSL转化成的SMT公式的可满足性.若结果是可满足的, 则证明ψ是不可满足的, 所求的解是ψ不被满足的实例.若验证结果是不满足的, 则说明在n步之前ψ是被CCSL约束满足的.
LTL公式转换成SMT公式分为两种.
● 第1种是δ为限界调度, 根据LTL的语义, 对于LTL公式ψ, 以G(ψ1∧ψ2)为例, 我们用公式
● 第2种是δ为周期调度, 比第1种情况较为复杂.其主要思想如下:用公式
结合第3.1节, 对于CCSL约束集Φ, 我们可以通过LTL公式对其时间属性进行模型检测.令ψ表示该LTL公式, 若⟦Φ⟧∧¬⟦ψ⟧是不可满足的, 则证明该约束集具有ψ表示的时间属性.当然, 我们通常设置一个边界值n, 用公式⟦Φ⟧n∧¬
为了使以上对于CCSL形式化验证与分析的方法有更好的可重复性和扩展性, 我们将其集成于一个原型工具, 其UML活动图如图 5所示.
工具的核心思想是:根据各个形式化方法将给定的CCSL约束、LTL公式转换成对应的SMT公式, 并放入SMT求解器中求解, 最终得到结果.它具有以下几点功能.
(1) 在转换前需要输入运行参数:程序超时时间, 防止运行时间过长而不能终止的情况; SMT求解器的选择, 可以选择使用Z3还是CVC4求解SMT公式; 边界值的设定, 当为0时表示无界的检测, 一般我们会输入个正整数作为检测的界;
(2) 对于输入的CCSL约束集合, 选择需要进行的操作, 如果需要LTL模型检测, 则要输入LTL公式.根据不同操作, 工具自动进行转换成对应的SMT公式并求解;
(3) 对于SMT求解器返回的结果进行处理, 不仅提示有没有解, 并且对于满足的情况画出结果, 整个工具采用图形化界面, 具有较强的可操作性;
(4) 采用基于nodejs的跨平台框架electron进行开发, 使得工具便于维护与移植.
图 6是工具在死锁检测时的页面截图, 展示了该原型工具在参数设置、公式输入和结果处理上的交互逻辑.
5 相关工作
对于CCSL约束的形式化分析方法的相关工作大多基于状态迁移系统与自动机原理.这些方法的优势在于可以利用现有的验证工具对CCSL验证分析.然而受限于目标模型的表达能力, 有些工作中只考虑了部分CCSL约束关系.另外, 由于对应的验证工具只能实现某种验证与分析, 无法对CCSL进行其他方面的分析.例如:Yin等人提出在Promela里对CCSL操作符进行转换[7], 然后用Spin工具进行模型检测; Gaston等人是将其转换成Büchi自动机[8], 然后比较CCSL与时态逻辑的表现.但这两个方法仅考虑了CCSL安全子集.Yu等人提出用SINGAL做CCSL的转换[18], 但也仅包含一部分, 并且SINGAL依赖三界逻辑.Suryadevara等人是将其转换为时间自动机[9], 但UPPAAL只能验证CCSL安全和物理时间的那部分约束.Mallet等人提出基于状态的CCSL语义并将每个约束转换为一个迁移系统[6], 然而一些如Precedence, Supremun这样的约束并不能用有限状态迁移系统表示.Zhang等人用Maude定义了一套CCSL可执行语义[10]进行仿真和模型检测.
本文提出的方法是将CCSL约束转换为SMT公式并进行统一化求解.本文提出的方法不是单一的针对某个问题而展开, 而是系统性地将多个问题统一而有效的解决.虽然该方法在不设置界的情况下满足性问题同样不能完全得到解决, 但是基于SMT求解器的高效性及其在有界条件下在不同分析中的应用, 基于SMT的方法依然是对CCSL形式化分析的有效方法之一.
已经有工作[16, 17]将LTL公式转换成SAT公式, 它们将有限状态自动机模型转换成命题逻辑公式, LTL公式的转换考虑到两种情况:一种是路径里没有循环, 另一种是存在循环, 同本文提出的对限界调度和周期调度的验证方法思路基本一致.不同之处有两点:其一是模型不同, 本文基于CCSL的调度模型; 其二是转换成公式为SMT公式.
6 总结以及未来工作本文提出了一种基于SMT的统一的CCSL形式化分析方法并集成于一个原型工具, 介绍了该方法在CCSL形式化分析中多种不同的应用, 包括有效性证明、迹分析、死锁检测以及LTL模型检测.同时展示了他们在具体实例中的应用.实验结果和数据说明了基于SMT的方法对CCSL形式化分析的有效性及高效性.
在本文工作的基础上有更多的工作值得研究:如何自动确定合适的边界值、如何将描述CCSL约束时间属性的CTL公式转换成SMT公式等.另外, 拟将该方法应用于工业案例中更复杂系统的验证, 以检验该方法在实际工业案例中的有效性.此外, 原型工具也需要进一步完善用于复杂系统的CCSL建模与分析, 如引入图形化操作实现对CCSL约束的定义、对验证结果进行图形化表示使其更容易理解等.
本文中, CCSL约束有效性证明采用的是对证明的公式取反证明其不可满足的方法.受限于转化的公式的可满足性问题的不可判定性, 这种方法是不完全的.K-induction是另一个潜在的方法, 是基本数学归纳证明方法的扩展, 形式化验证工具SAL实现了基于K-induction方法的定理证明[21].利用K-induction实现CCSL某些定理的证明可避免设定边界值证明的局限性, 这又是一个值得深入研究的工作.
[1] |
Object Management Group. UML profile for MARTE: Modeling and analysis of real-timeembedded systems. 2011. |
[2] |
André C. Syntax and semantics of the clock constraint specification language (CCSL). Research Report, RR-6925, INRIA, 2009. |
[3] |
Mallet F, André C. On the semantics of UML/MARTE clock constraints. In: Proc. of the IEEE Int'l Symp. on Object/Component/Service-Oriented Real-Time Distributed Computing (ISORC 2009). IEEE, 2009. 305-312. [doi:10.1109/ISORC.2009.27] |
[4] |
Kang EY, Schobbens PY. Schedulability analysis support for automotive systems: From requirement to implementation. In: Proc. of the 29th Annual ACM Symp. on Applied Computing. ACM Press, 2014. 1080-1085. [doi:10.1145/2554850.2554929] |
[5] |
Mallet F. MARTE/CCSL for modeling cyber-physical systems. In: Proc. of the Formal Modeling and Verification of CyberPhysical Systems. Springer Fachmedien Wiesbaden, 2015. 26-49. [doi:10.1007/978-3-658-09994-7_2] |
[6] |
Mallet F, De Simone R. Correctness issues on MARTE/CCSL constraints. Science of Computer Programming, 2015, 106: 78–92.
[doi:10.1016/j.scico.2015.03.001] |
[7] |
Yin L, Mallet F, Liu J. Verification of MARTE/CCSL time requirements in Promela/SPIN. In: Proc. of the 201116th IEEE Int'l Conf. on Engineering of Complex Computer Systems (ICECCS). IEEE, 2011. 65-74. [doi:10.1109/ICECCS.2011.14] |
[8] |
Gascon R, Mallet F, Deantoni J. Logical time and temporal logics: Comparing UML MARTE/CCSL and PSL. In: Proc. of the 201118th Int'l Symp. on Temporal Representation and Reasoning (TIME). IEEE, 2011. 141-148. [doi:10.1109/TIME.2011.10] |
[9] |
Suryadevara J, Seceleanu C, Mallet F, et al. Verifying MARTE/CCSL mode behaviors using UPPAAL. In: Proc. of the Int'l Conf. on Software Engineering and Formal Methods. Berlin, Heidelberg: Springer-Verlag, 2013. 1-15. [doi:10.1007/978-3-642-40561-7_1] |
[10] |
Zhang M, Mallet F. An executable semantics of clock constraint specification language and its applications. In: Proc. of the Int'l Workshop on Formal Techniques for Safety-Critical Systems. Cham: Springer-Verlag, 2015. 37-51. [doi:10.1007/978-3-319-29510-72] |
[11] |
Zhang M, Mallet F, Zhu H. An SMT-based approach to the formal analysis of MARTE/CCSL. In: Proc. of the Int'l Conf. on Formal Engineering Methods. Springer Int'l Publishing, 2016. 433-449. [doi:10.1007/978-3-319-47846-3_27] |
[12] |
Barrett C, Stump A, Tinelli C. The smt-lib standard: Version 2. 0. In: Proc. of the 8th Int'l Workshop on Satisfiability Modulo Theories. Edinburgh, 2010. 13-14. |
[13] |
De Moura L, Bjørner N. Z3: An efficient SMT solver. In: Proc. of the Tools and Algorithms for the Construction and Analysis of Systems. 2008. 337-340. [doi:10.1007/978-3-540-78800-3_24] |
[14] |
Cohen B, Venkataramanan S, Kumari A. System Verilog Assertions Handbook-For Formal and Dynamic Verification. Vhdlcohen Publishing, 2005.
|
[15] |
Biere A, Cimatti A, Clarke EM, et al. Bounded model checking. Advances in Computers, 2003, 58: 117–148.
|
[16] |
Cimatti A, Pistore M, Roveri M, et al. Improving the encoding of LTL model checking into SAT. In: Proc. of the Int'l Workshop on Verification, Model Checking, and Abstract Interpretation. Berlin, Heidelberg: Springer-Verlag, 2002. 196-207. [doi:10.1007/3-540-47813-2_14] |
[17] |
Zhang W. SAT-Based verification of LTL formulas. In: Proc. of the FMICS/PDMC. 2006. 277-292. [doi:10.1007/978-3-540-70952-7_18] |
[18] |
Yu H, Talpin JP, Besnard L, et al. Polychronous controller synthesis from MARTE CCSL timing specifications. In: Proc. of the 9th ACM/IEEE Int'l Conf. on Formal Methods and Models for Codesign. IEEE Computer Society, 2011. 21-30. [doi:10.1109/MEMCOD.2011.5970507] |
[19] |
Zhang M, Ying Y. Towards SMT-based LTL model checking of clock constraint specification language for real-time and embedded systems. In: Proc. of the 18th ACM SIGPLAN/SIGBED Conf. on Languages, Compilers, and Tools for Embedded Systems. ACM Press, 2017. 61-70. [doi:10.1145/3078633.3081035] |
[20] |
Zhang M, Dai F, Mallet F. Periodic scheduling for MARTE/CCSL: Theory and practice. In: Proc. of the Science of Computer Programming. 2017. [doi:10.1016/j.scico.2017.08.015] |
[21] |
De Moura L, Owre S, Rueß H, et al. SAL 2. In: Proc. of the Int'l Conf. on Computer Aided Verification. Berlin, Heidelberg: Springer-Verlag, 2004. 496-500. [doi:10.1007/978-3-540-27813-9_45] |
[22] |
Jin JW, Ma FF, Zhang J. Brief Introduction to SMT solving. Journal of Frontiers of Computer Science and Technology, 2015, 9(7): 769–780(in Chinese with English abstract).
http://mall.cnki.net/magazine/Article/KXTS201507001.htm |
[22] |
金继伟, 马菲菲, 张健. SMT求解技术简述. 计算机科学与探索, 2015, 9(7): 769–780.
http://mall.cnki.net/magazine/Article/KXTS201507001.htm
|