未来工作：

liveness; implicit; 数据集；抽象方式合并；抽象规则配置；缓解谓词爆炸；concurrency的说明; 代码简化工作；给出能修复的漏洞种类

代码未实现：

delay之后的抽象不能取值钱的值，last状态为安全如何定义安全，VAR里的函数类型建模
不被设备执行影响的延时自然属性，比如下雨，那么被设备影响的延时自然属性，比如温度，烟雾？？？
不被设备执行影响的非延时自然属性，比如
被设备影响的非延时自然属性，比如光照
一次新增多条规则而不是一条
fix_rule初始化为{}会不会导致如果满足属性，出现Bug
LTL在非限界的布尔编码
新规则要排除老规则
ASSIGN_NEW_RULE里对数值类的处理是一个值一个谓词，这样不行
某个概念如state space在background里一笔带过，后面可不可以不解释？？

疑问

符号的定义重复了
符号的字体清不清楚
反属性推理想和整体取反作符号区分
图、表、公式、算法的引用
图片大小
系统结构图和算法概述的位置
单复数，the，句子开头字母才大写
检测种类只体现在实验，不体现在代码
基于什么什么的描述，推出一个结论，那么这个结论可以不可以放到描述那些，虽然前面没用到

整体代码细节

TAP规则按照action作字典

输入：entity_attribute_list 、entity_rule_list、spec_list
for spec in spec_list:
  规则交互模型构建ModelBuilder（其中包含属性筛选）
  规则交互漏洞检测ModelChecker
  反属性推理
  if 推理成功:
    修复成功，返回修复后的规则
  else:
	无法修复

在安全属性，反属性检测后都对CEX进行complete_state()
第一次抽象是CEX引导的，之后是CEX以及上次的抽象过程
无法解决可能是安全属性的优先级问题如sleep和away
一个谓词等于 flag->取值

% 算法写半页的1/3页到3/4页
% 算法解释加上目的，不说函数
% 5行就可以做算法

规则交互模型构建的代码细节

筛选实体属性自动机变量定义

channel-based interaction config :

从筛选属性中选出有物理影响的
CONFIG(包括运作和不运作)+THRESHOLD
自然延时属性自动机变量定义 __count 实现自动变化的环境谓词
对于不被设备执行影响的延时自然属性，比如下雨变化靠__count，被设备影响的延时自然属性没有状态时靠__count，否则靠设备的物理影响<threshold则每次加，大于则回归之前状态

不被设备执行影响的非延时自然属性，比如？？？
被设备影响的非延时自然属性，比如光照？？？

last值为安全保证可以从第一个状态触发
大多数数据结构都是字典或者[[[],[] ]一条rule，[]第二天]

延时变量

MODULE RUNIN

规则交互模型抽象的代码细节

flag->取值抽象为一个谓词P(取值)，只有真假
CEGAR包括模型抽象和反属性验证
class变量清零
单trigger的情况不加INVAR_flag
LAST变量的处理，安全属性中的和属性外的，保证初始状态能触发
对LAST变量的引入

模型抽象

除了正常的建模外

1+3n是 present
2+3n是new
3+3n是delay

build_INVAR constraints
value flag: toint(original_flag_rule0_weather.rain_0) + toint(original_flag_rule0_weather.rain_1) != 2 对现有和新增
如果是现有，排除已有谓词，如果是新增，排除当前谓词
trigger flag 新规则步骤加，一次一条，排除当前谓词

delay的抽象在VAR实现
在建模延时变量时，将取值范围设置为0或延时
predicate_flag
抽象只针对property里的entity

find_assign_before_violating_state
predicate(attribute):[0,1,2,3,4]

abstract_time_ASSIGN
__Extended_rule_flag_ASSIGN
get_var_value

抽象精化

build_INVAR: class.INVAR.test_list之前的取值

在之前的build_VAR加入：
初始值定格
step和step_upperlimit
不被设备执行影响的非延时自然属性，比如
不被设备执行影响的延时自然属性，比如下雨，被设备影响的延时自然属性的也是同样方式

修复对比

Thier work最接近我们的工作，但也有差异
没有明确提出反属性，且简单，之前是更大空间需要反属性，我们是反属性需要更大空间，所以Trigger、Condition、Action都要变

Previous work searches potential TAP patches by changing
trigger-states of existing TAP rules in three ways: (1) deleting
a conjunction clause; (2) adding a conjunction clause that
appears in the LTL/CTL policy（只加了属性中出现的，N-gram?）; or (3) modifying numerical
parameters. Consequently, they cannot synthesize patches that
change TAP rules’ trigger events or rule actions（从状态机模型的角度，推导出都要变）, not to mention creating new TAP rules from scratch.
The end-user property specification interface of previous work [22] only accepts
“[states] shall not happen”, missing many common desires.比如G（F），liveness
有些安全属性没有说明

修复算法：初始值固定
Salus按照所编写的顺序执行规则来解决相互冲突的设备命令

修复是user-facing

共享环境属性，包括环境属性影响，在建模时完成（共同区域+same channel），temperature里加一个trasition
不仅是共享，而且有共同，我没咋说共同，比如温度湿度关联，归于共同作用
本文只说了devices can influence the readings of sensors in the same logical space.而且没说温湿度关联

定位方法：用形式化的方法定位错误的用户逻辑，他这里只指反例

将系统逻辑转为等价方程式解SMT，方程右侧是违反的约束？
对于没有LTL和CTL语法的琐碎策略

修复算法：
首先，尝试现有，它试图确定是否可以更改任何自动化规则参数（数值，枚举）。
其次，尝试新的，它试图看看是否可以引入额外的自动化规则（增删trigger）。然后，根据用户的偏好，ActAxdaod制定一个解决方案，然后提交给用户批准。adding or deleting rules’ triggering conditions
IF livingroom.temp <= 18 THEN livingroom.heater = on 加没人的条件

尝试过的值下次不再尝试，通过invariant
在这里插入图片描述
The basic idea is to re-use model checkers’ ability of solving parametrized equations

Rule:
IF kitchen.CO2 > 1000 THEN kitchen.fan = on

property:
kitchen CO2 level cannot exceed 1000 ppm, globally

FIX RULE：
IF kitchen.CO2 > X THEN kitchen.fan = on

Prioritizing Solutions.
会求解出多个值，由用户选择或者根据偏好选择（用决策树）
数值选择选接近原来的，定义一定范围内的

Rule:
IF livingroom.temp <= 18 THEN livingroom.heater = on

property:
if no one is in the living room,then heater should always be off
增删的trigger来源于policies provide hints on
by considering all conditions in the policies but not in the rules.而我们考虑了规则里的

FIX RULE：
IF λ1 ⇒ (livingroom.temp <= X) AND
λ2 ⇒ (livingroom.occupancy == Y)
THEN livingroom.heater = on
λ1 p->q 非p或q，p为1则启用条件，p为0则等于加没加都为TRUE

在这里插入图片描述