Page 80 - 《软件学报》2021年第12期

3744 Journal of Software 软件学报 Vol.32, No.12, December 2021

实体-能力抽象 W,事件筛选策略P=P default ;
输出:该事件是否应被排除.
1. C E =E 形如(e,c,V s ,V d )?EventCond(M c ,V s ,V d ):True
//从 M c 中获取 V s →V d 的事件转移必要条件
2. Assertion = SysStateAssert P (,! , ,E ΨΨ C E )
//P default 为 E 发生前!Ψ为真、E 发生后Ψ,为真
//事件发生前后 C E 成立
3. SATResult=Z3.Satisfiable(Assertion,W)
4. if SATResult=“UNSAT” then return true
5. else return false
算法 5. 同一动作序列的 EE 规则生成(SameActionsRules).
输入:筛选后的事件集E′,不兼容条件Ψ ,动作序列A j ,执行前提 C j ,系统实体-能力抽象 W;
X
E
输出:与动作序列A j 相同的规则集合 \ .
A
1. if A j 为空序列 then return
E
2. \ A =∅

′
3. for each E in E do
4. C E =E 形如(e,c,V s ,V d )?EventCond(M c ,V s ,V d ):True
5. C Ψ= X and C jPostcond ()E //在事件 E 发生后,Ψ and C j 成立的条件
|
X
6. Assertion = SysStateAssert P (,! , ,E Ψ C C E ) //默认策略仍假设事件发生前!Ψ为真
7. if Z3.Satisfiable(Assertion,W)=“UNSAT” then continue
8. if A j =“IMPOSSIBLE” then error “无法保证翻译规则的一致性”
)
9. \ A E = A E ∪ \ ({ }, ,EC A
j
10. end for
S
算法 4 旨在判断事件 E 可否发生并在发生后使得Ψ( \ 不兼容的条件)为真(进而导致Ψ对应的某个动作序
X
列的执行),需要根据筛选策略P做关于系统抽象状态的可满足性判定.筛选策略从保守到激进有多种策略:激进
的策略需要对事件发生之前的系统状态做出更强的假设,而保守的策略只需要相对较弱、能够更快判定的假
S
S
设.本文提出的默认策略P default 为:事件发生前Ψ为假( \ 兼容),事件发生后Ψ为真( \ 不兼容),且事件发生前
X X
后 V s →V d 的事件转移条件 C E 成立,则该事件不会被排除.
继续以图 4 的规则组 \ X S 2 为例,其不兼容条件为Ψ X 2 .对于事件 E=(模式,状态,{离家模式},{回家模式}),由于
M 模式状态的离家模式到回家模式的转移没有必要条件,故 C E =TRUE.按照默认筛选策略,将模式.状态在事件发生
前后的值分别代入!Ψ X 2 和Ψ X 2 ,则 Assertion 为“!(离家模式=回家模式 AND 温湿度传感器.温度>28°C AND (电

扇.开关!=开 OR 电扇.风速!=低)) AND (回家模式=回家模式 AND 温湿度传感器.温度>28°C AND (电扇.开
关!=开 OR 电扇.风速!=低))”.这一断言是可满足的,所以事件 E 不被排除,将交由 EE 中间表示生成处理.
以图 4 中 \ S 规则组为例,本文的默认事件筛选策略与系统抽象状态的可能转移之间的联系如图 5,左上方
X 1
S
是以 G 中的若干规则组的状态为局部视角时系统抽象状态的转移图,按照一次一个外部事件、一次执行一条
规则的系统执行假设,不会发生的系统抽象状态转移用点线表示.按照当前默认的事件筛选策略P default ,认为可
能到达 \ S 的不兼容状态的状态转移由右上图中 4 条深色的系统抽象状态转移边表示(与左上图对比,边③是
X 1
在当前系统抽象和规则执行假设下不会发生的状态转移),但是在左下方粗粒度的系统抽象状态转移图上,却对
应着相同的转移边.使用较保守的事件筛选策略的缺点就在于可能未排除边③这样的边,进而存在生成出不能
执行到的规则的可能性.需要注意的是:EE 规则中的事件和图中的系统抽象状态转移边不一定一一对应,能够