随着物联网、人工智能与5G等创新技术驱动的万物互联时代的到来, 智能家居作为物联网的重要应用场景之一, 正快速进入千家万户.智能家居令家庭中的各种设备互联互通, 使用户实现设备的自动控制、远程控制和可编程控制, 甚至可以根据历史经验主动进行自动化服务.根据MarketWatch发布的报告^[1], 2016年, 全球智能家居市值556.5亿美元, 预计2025年将达到1 742.4亿美元; 同时, 中国的智能家居市场也在快速发展, 据艾瑞咨询发布的报告^[2], 2017年, 中国智能家居市场规模为3 254.7亿元, 预计2020年将达到5 819.3亿元.

为管理种类和规模不断增加的智能设备, 国内外主要领导厂商纷纷推出智能家居平台, 如三星的SmartThings、Amazon的Alexa、Google的Home、小米的米家、华为HiLink、云端规则定制平台IFTTT(“IF This Then That”)^[3]等, 但它们几乎不开源并且仅支持相关品牌的设备, 限制了用户所能管控的设备类型及范围; 在开源的智能家居平台中, 基于Python3的HomeAssistant^[4]相对成熟, 支持多种操作系统/平台, 集成了IFTTT、GoogleAssistant、MQTT等产品/功能.这些智能家居平台将要管控的设备抽象化, 通过建立通信标准以及API互联等方式连接设备和app, 采用“触发-动作编程”(trigger-action programming, 简称TAP)^[5]支持用户定制规则以指定系统行为.但我们通过多次调研发现: 现有TAP虽足以满足终端用户表达简单的自动化任务, 但灵活性不足, 难以支持更复杂的用例^[5-8].

TAP规则(如IFTTT)典型地将单个触发器(trigger)与单个动作(action)关联起来, 例如“如果开始下雨, 则关窗”.然而, 许多常见行为需要TAP提供更强的表达能力, 如对空调等复杂设备的设定、对门锁窗户等安全攸关设备的可靠设定、对夜灯/咖啡机等设备的工作持续时间设定等.为支持用户的日常需求, 不同的智能家居平台提供不同的支持, 例如引入and连接多个触发器^[5]或者连接多个触发器和多个动作(如Stringify^[9])、用更一般的and/or组合多个触发器或多个动作(如HomeAssistant)、增加对触发器的条件过滤(如Microsoft Flow^[10], Zapier^[11]和HomeAssistant)、增加“状态保持时长”的表达能力(如SmartRules^[12])、支持自定义的事件/服务(如HomeAssistant).各种TAP扩展丰富了可定制性, 但是也存在语义不清晰、编写复杂等缺陷, 不便于用户使用.

随着设备数量的增加, 其交互也随之增多, TAP编程出错的可能性也会增加.针对这类问题, 一些研究如BuildingRules^[13], IRuler^[14]等提供对某些TAP编程缺陷的检测; AutoTap^[15]能由线性时序逻辑表达的设备性质合成某些TAP规则, 从而避免用户直接编写TAP规则; AutoTap和Menshen^[16]还提供有限的错误修复功能. Brackenbury等人^[17]首次提出和规范可用于TAP规则触发器的3种时序范式Event-Event, State-State和Event- State, 并总结了TAP可能存在的10种编程缺陷.

针对智能家居系统面临的挑战, 本文研究易写易改、支持多触发器-多动作、支持状态保持描述等能力的TAP规则的表示, 然后构建支持这种规则表示的智能家居自动化框架.在TAP规则的表示方面, 触发器和动作均可以分为(纯)状态型和事件型.本文首先系统分析和总结了各种TAP编程范式以及它们引起的缺陷种类、原因和检测/修复现状, 指出了改进TAP的可能渠道; 然后, 针对用户不易分清事件和状态、不易写全规则所要考虑的情况组合以及“Event-trigger Event-action”(EE)风格的规则冗长、更改琐碎等特征, 本文提出以“State-trigger State-action”(SS)为基础构建面向终端用户易写易改的、具有丰富表达能力的具体SS规则范式.在自动化框架构建方面, 鉴于HomeAssistant(简称HA)相对成熟和开源, 支持多种平台和多种设备及服务集成方式, 提供以Event为核心的宽泛TAP配置, 本文以它为基础构建支持SS规则范式的智能家居自动化框架SSRules.针对Brackenbury等人^[17]指出的10种TAP缺陷, 采用SS规则范式能天然排除时间窗错误和翻转触发器这2种缺陷, 完全避免优先级冲突; 结合SSRules的实现策略, 能部分解决或消除安全默认偏差、非瞬时动作、重复触发这3种缺陷, 并附带改善缺少反向动作的缺陷; 对于无限循环和不确定时序这两种缺陷, 可以通过模型检查等方法在规则转译成HA之前避免; SSRules尚不能解决矛盾的动作这种缺陷.本文的主要贡献如下:

(1) 系统分析和总结了TAP编程范式及其编程缺陷, 指出了改进TAP的几种可能渠道, 为我国智能家居领域从业者和软件研发人员全面了解TAP编程、缺陷及改进提供了参考资料;

(2) 提出以“State-trigger State-action”为基础构建易写易改、有丰富表达力的TAP编程范式.SS规则范式以实体-能力抽象为基础, 按动作实体将规则分组、组内按序优先, 有效避免了优先级冲突; 它区分只读和可控能力, 提供4种表示历史状态的算符, 并方便表达在指定状态/状态保持下对多种能力的期望;

(3) 引入能表达事件型智能家居执行引擎的独立“Event-trigger Event-action”(EE)中间表示, 基于HA构建智能家居自动化框架SSRules, 它能将SS规则集合经EE规则表示转译成HA规则, 利用Z3定理证明器^[18]进行触发事件的筛选和规则化简, 并提供运行时子系统动态感知设备变化和检查规则执行的有效性;

(4) 实现了智能家居模拟器和SSRules原型系统.对10组测试场景, 用SS范式编写所需的规则条数比转译和合并后得到的EE范式规则数平均减少了60%左右; 在模拟实验环境下, 最终生成的HA规则的运行时检查都未发现连续异常, 并且所记录到的瞬时异常(小于总检查次数的0.3%)经查阅日志均为网络延迟引起.

本文第1节对现有TAP编程范式及其引起的缺陷、易用性以及缺陷检查和修复现状进行总结.第2节提出智能家居自动化框架的设计目标, 对以HA为底层基础、以SS规则范式为用户输入的智能家居自动化框架SSRules的总体设计进行总结.第3节详细讨论SS规则范式的定义及其到HA规则的转译方法.第4节介绍基于HA构建的智能家居模拟环境, 并在该模拟环境上评估了SSRules的有效性.第5节和第6节分别对相关工作和本文的工作进行总结.

1 TAP编程范式及缺陷分析

为了满足终端用户灵活多样的需求, 大多数智能家居平台都提供特定的TAP编程接口用于对智能设备和/或服务进行编程, 以定制智能家居系统的行为.本节首先对TAP编程范式进行了详细分析, 然后系统总结分析了可能导致TAP缺陷的原因, 最后简要总结改进TAP的可能渠道.

1.1 TAP编程范式概述

TAP的表达能力及易写易改性, 对智能家居的推广和普及至关重要.目前最流行的TAP接口是IFTTT在线服务^[3], 它允许用户创建程序、自动执行由单个事件触发的动作, 尽管IFTTT应用广泛, 但其表达能力非常受限.

● 多触发器、多动作

根据Ur等人的用户调查^[5], 22%的编程行为需要不止一个触发器或动作, 并且触发器和动作在用户期望的行为中的组合也更为多样化.因此, Ur等人引入“and”连接触发同一动作的多个事件, 例如“IF窗户是开的and在下雨”就触发“关窗”.Zapier^[11]允许将多个动作绑定到一个触发器; Stringify^[9]支持形如“If This and This, Then That and That”的规则.HA^[4]还允许定制只要多个触发器中任意一个被触发就执行的规则.

● 条件过滤与工作流控制

Zapier和HA提供过滤器, 支持对触发器的进一步(and/or)条件过滤.例如: 可以在触发器“接收邮件”后追加过滤器“主题包含X and来自Y”; MicrosoftFlow^[10]不仅提供多步骤的工作流, 还提供If-then-else条件过滤、For-Each和Do-While循环等; HA允许定制包含“call service”动作、自定义事件和自定义触发器的规则, 允许开发者编程实现各种服务.Flow和HA提供的这些功能非常强大, 但是对终端用户编程的能力要求高, 且缺少对用户配置的有效性检查.

● 区分事件(event)与状态(state)

IFTTT的“if this then that”易被理解为通用编程中的if-then语句, 而其实际语义却等价于事件驱动编程. Huang等人^[6]认为: 把IFTTT隐喻成if-then会有歧义, 这种歧义会给用户带来困难.由此提出用事件和状态区分触发器: 事件是瞬时信号(如“温度降到10℃以下”), 而状态是可随时评价的布尔条件(如“在下雨”).Brackenbury等人^[17]进一步将动作分成事件(在特定时刻发生, 如“关灯”)和状态(一段时间内设备的期望状态, 如“灯应亮着”)两类.这种区分事件和状态的TAP看似消除了一些歧义, 潜在简化了系统实现中对TAP规则的理解, 但是研究表明: 终端用户往往很难清晰区分事件和状态^[6], 且它们的组合又引出新问题.

● 事件和状态的组合

事件和状态在组合时有以下语义: 多个状态s_i的合取是另一个状态s, 仅当每个s_i为真时s为真; 状态s与事件e的合取是在s为真时e同时发生的另一个事件e′; 两个事件e₁和e₂的合取是与e₁和e₂同时发生的另一个事件.然而在智能家居系统中, “事件同时发生”无论是理论还是实际都不太可能发生.Brackenbury等人^[17]提出了3种多触发器组合的时序范式: Event-Event, Event-State和State-State, 并将它们与动作组合成表 1所示的4类TAP规则.其中: Event-Event时序范式引入WITHIN时间窗口子句来描述不能同时发生的事件, 并提供AFTERWARDS指定事件次序; Event-State时序范式将触发器限制为一个带若干状态的事件.这两类触发器均触发事件型动作, 也是真实智能家居系统主要采取的方式.State-State触发器范式组合多个状态并且状态会在一段时间内满足, 故自然地触发状态动作; 考虑到影响同一设备的多条规则的多个状态可能同时为真(如控制空调的模式), 故State-State→State范式需要包含优先级来解决冲突.此外, 对于少数不能直接表示为状态型的离散事件动作(如“记录日志”), State-State时序范式会触发事件动作.

● 状态保持性描述

Huang等人^[6]将动作分成瞬时动作(如“发邮件”)、在固定时间完成的动作(如“冲泡咖啡”)、包含改变状态的持续性动作(如“开灯”), 这给智能家居系统提出了描述和实现状态保持特性的需求.SmartRules提供“状态保持”的表达, 可以创建“如果门开着有5分钟就通知”之类的动作.HA提供的trigger可以定时, 虽然其action没有直接提供保持时长的表示方法, 但是它提供的callservice动作潜在允许开发者编写处理状态保持时长等服务的能力, 因此也可以实现类似状态保持的表达.

1.2 TAP规则的缺陷分析

用户在编写TAP规则时很容易出错, 原因在于智能家居设备众多、用户期望的行为复杂多样、智能家居设备之间存在大量的交互^[19], 单个设备会直接或间接影响到其他设备.人的行为也会影响设备状态, 而人的即使看似简单的行为也可能会引起背后复杂的设备行为; 且人的行为与需求并非一成不变, 在不同的场景需求下, 很可能会造成对已有规则的破坏^[20].由于智能家居的用户通常缺乏编程相关的训练, 为降低编程门槛, TAP过分简化了操作界面^[6], 从而使程序的表达能力变差, 这进一步恶化了TAP对复杂行为的可解释性.

Brackenbury等人^[17]通过用户调查, 总结出可能出现在TAP的10种缺陷, 包括:

(1) 4种缺陷已被发现且详细讨论

① 优先级冲突(priority conflict), 仅在采用State-State→State时需要对作用于同一设备的多条规则进行优先级排序, 而用户往往难以按自己的意图正确设置规则优先级^[21].这种缺陷已被TAP文献广泛讨论^{[7, 13, 22-24]}, 可以通过静态分析来检测;

② 安全默认偏差(secure-default bias)发生在用户默认系统处在安全状态^[21](例如夜间锁住窗口), 但广泛部署的Event–State设备没有默认状态, Yarosh等人详细讨论了门锁的这种缺陷^[21];

③ 非瞬时动作(extended action)源于动作发生在一段时间而不是瞬时的(如冲泡咖啡);

④ 缺少反向动作(missing reversal)发生在用户创建了一条执行某动作的规则而没有写撤销该动作的规则时, 例如写了“IF进客厅THEN开灯”但忘写离开关灯的规则, 但用户可能认为系统会自动关灯^{[6, 21]}.Huang等人^[6]详细讨论了缺陷③和缺陷④, 并对系统接口提出改进建议.缺陷④可以通过静态分析检测, 但不总能被修复.

(2) 3种缺陷被提及

⑤ 无限循环(infinite loop)的原因是规则相互触发, 这种缺陷在机器人终端用户编程中常被遇到^[6];

⑥ 重复触发(repeated triggering)指用户希望规则仅触发一次, 但却触发多次.这种缺陷主要出现在State-State范式下因状态触发器持续为真导致规则触发多次.Cao等人^[25]在mashup编程工作中提及了这种缺陷;

⑦ 不确定的时序(nondeterministic timing)是由于系统处理同时发生的触发器的顺序不确定而导致.Huang等人^[6]简要讨论了TAP中存在的这种缺陷.

这3种缺陷均可以通过静态分析来检测, 但是实际系统无法鉴别重复触发是否是用户的有意行为.缺陷⑤和缺陷⑦还可以通过动态分析检测.

(3) TAP新增缺陷

⑧ 矛盾的动作(contradictory action)指的是长周期内在矛盾的动作间无限循环(例如加热和冷却之间不断交替);

⑨ 时间窗错误(time-window fallacy)是当用户在编写Event-Event范式的规则时忘指定时间窗时导致;

⑩ 翻转触发器(flipped triggers)是因用户难以指定触发器中哪部分是事件哪部分是状态而导致的.这种缺陷在静态或动态分析中都很难检测到.

表 2总结了上述10种缺陷的原因、引起缺陷的TAP编程范式、缺陷检查或修复方法.

10种缺陷中, 第①种、第②种、第④种、第⑨种、第⑩种归结为与用户预期不一样, 第③种、第⑦种为时序缺陷, 剩余3种为控制流缺陷.表中第3列的“All”表示表 1中的4类TAP规则都可能引起这种缺陷.从中可见: 第①种和第③种这两种缺陷仅存在于纯状态触发器的TAP编程中, 而第⑨种、第⑩种仅存在于含事件的触发器的TAP编程中.Brackenbury等人^[17]对这10种缺陷的进一步用户调查表明: 相比Event-State, 问卷参与者使用State-State能写得更正确, 而使用Event-Event则正确性要差些.

1.3 改进TAP的可能渠道

现有的TAP平台尚未能充分满足用户需求, 在实际运行中容易出现缺陷导致系统出错.综合分析现有智能家居系统及学术研究成果, 以下给出了几种改进TAP、减少编程缺陷的渠道.

(1) TAP编程范式

实际智能家居系统大都基于Event-State→Event规则范式来实现.相比于使用事件型触发器进行TAP编程, 使用纯状态触发器更容易让终端用户正确表达意图.即使使用相同的触发器范型和动作范型, 不同的TAP规则结构仍会影响TAP编程的表达能力、易用性和编程缺陷.现有解决方案中, 除了直接让终端用户写TAP规则, 研究人员还提出了不同的实现方案, 如:

● AutoTap^[15]允许用户输入设备的安全性质(可转化为线性时序逻辑公式)而由系统合成Event-State→ Event规则, 从而减少最终规则的缺陷, 但是存在合成效率较低、难以适用较多设备、安全性质不适合表达需求细节等不足;

● Zave等人^[24]提出让用户对设备按不同目的(如安全性、节能等)分别描述需求特征, 然后手工为特征建立状态机, 并根据它设计运行时的特征组合机制来实时控制执行器.如何由非形式的特征描述建立FSM以及解决特征冲突(或称特征交互)是其中的难点, 该方法目前只支持对几种设备的人工建模且仅支持“值设置”动作.

(2) TAP规则的检查与修复

改进TAP编程范式不可能完全消除编程缺陷, TAP平台仍需要一些额外的工具或方法来检查TAP规则的有效性, 并尝试修复规则.现有的方法大都针对Event-State→Event规则进行静态检查(如IRuler^[14], AutoTap^[15], MenShen^{[16, 22]})、动态检查(IoTGuard^[19])或规则修复(AutoTap, MenShen, TrigGen^[26]), 仅有极个别方案是基于状态触发的^{[21, 24]}, 这很大程度上是因为实际的智能家居系统是按事件驱动方式来运行的.表 3从多种维度比较了已有方法, 可以看出, Event-State→Event规则的修复存在搜索修复策略低效以及在不清楚用户意图的情况下仍需用户决策等局限性.而随着设备数增多, 这类规则及修复逻辑的可读/可理解性也在下降.此外, 由于网络延迟/重放攻击等, 也会使基于EE的智能家居系统执行不期望的动作.Wang等人^[27]提出, 通过分析日志中事件间的依赖来事后追因.

(3) 智能家居系统的实现

对TAP规则的静态检测和修复可以在规则实际运行前识别出部分规则缺陷, 并尝试手工/自动修复.但是如表 2第4列所说, 还有许多缺陷是静态无法检测, 或是由于难以判断用户意图从而无法确定缺陷是否存在.因此, 智能家居系统在实现时需要提供:

1) 给用户更多的提示和警告: 针对那些潜在有歧义、有冲突或已做动作不会被自动撤销等情况, 系统要给出用户易于理解的提示或警告;

2) 提供不易让用户混淆的选项供用户选择;

3) 提供运行时日志的记录, 需要权衡日志的存储量与事后推理的便利性;

4) 支持和提供含义更明确的顶层trigger-action结构, 等等.

2 SSRules智能家居系统总体设计

为使终端用户易于编程, 本文重点探索状态触发器-状态动作的TAP编程范式(简称SS规则范式), 并基于HA构建了支持SS规则范式输入的SSRules系统.SSRules在不改变HA规则执行引擎的基础上, 扩展提供更易被用户理解和掌握的规则表达方式以及对应的规则转译器.虽然SS规则范式尚不支持表达无状态或难以抽象出状态的事件动作, 但由于这类动作所占比重小、用户需求低, 因此, SSRules可以支持用户的绝大多数需求.未来可以设计专门的机制, 将这些无状态的事件动作加入到SSRules系统中.本节首先简要介绍SSRules的设计目标, 然后分析HA的关键特征, 最后给出SSRules总体架构以及所引入的Entity-Capability抽象.

2.1 设计目标

智能家居正进入寻常百姓家, 为了让SSRules满足用户的不同需求, 现阶段至少应围绕如下目标设计.

G1. 易写易改.针对用户调查^{[5, 6, 15, 17]}反映的TAP规则编写和修改的问题, SSRules应提供让无编程经验的终端用户快速学习并正确使用的编程范式, 方便表达所期望的智能家居系统性质, 且在需求变化时容易修改;

G2. 可管可控.SSRules系统应能提供按终端用户的有效需求对来自不同厂商的设备实时监测与控制, 感知系统中动态加入和退出的管控对象, 而不能只支持特定厂商的设备和仅提供极其有限的监测能力;

G3. 异常检测.智能家居系统的可靠性受限于网络、设备故障等不定因素, 而用户希望系统提供实时反馈以及对系统更多的控制感.因此, 系统需要能够帮助用户监视运行状况, 并将异常信息反馈给用户;

G4. 协调需求.作用于同一设备的多种需求存在冲突, 是智能家居中的常见现象.系统要提供简单的处理方式, 便于用户协调好同一设备存在冲突的多种需求.例如希望灯在夜间关闭, 但是有人经过则应以较低亮度打开一段时间, 如果遇到紧急情况(如厨房着火)则应当完全打开;

G5. 多方信息.智能家居系统的功能边界应当不限于家庭的物理空间.系统不仅要能够处理家庭中存在的物理设备, 也要能处理虚拟传感器和虚拟的设备, 如情景模式、天气、时钟等.

2.2 HomeAssistant(HA)

本文的研究重点为探索TAP编程的表示及其在现有执行引擎的实现, 同时提供一定的规则有效性检查功能.因此, 为更有效地实现G2和G5涉及的目标, SSRules需要选择成熟开源的智能家居执行引擎来实现与各种(虚拟)设备的连接、实时监控、动态感知以及自动化管理等.

在开源智能家居系统中, HA是基于Python的成熟智能家居开源系统, 能部署在任何能运行Python 3的机器上, 从树莓派到网络存储, 还可以使用Docker部署到其他系统上.它主要根据automations.yaml等配置文件实现集中化的智能家居设备管理, 设备支持度高, 具有自动化、群组化、UI客制化等高度定制化设置; 同时, 其开发者数量、版本更新速度在所有开源项目中也都属于佼佼者.因此, 我们最终选取HA作为SSRules的执行引擎.

● 灵活的集成方式

在HA中, 物理设备和虚拟设备均被抽象为实体, 带有状态的实体可以与状态对象关联.天气、太阳角度等均为HA预置的虚拟实体; 通过用户自定义或第三方集成, 还可以实现如模式开关、空气质量、用户位置等虚拟传感器和动作器.实体上可以执行的动作被抽象为服务调用, 除了HA自带的值变化事件、服务调用事件等事件类型, 第三方集成也能够发布其他自定义的事件.采用HA可以自然地支持目标G5.

● 设备的动态管理

HA接入设备的方式之一是MQTT Discovery, 它提供对基于MQTT(message queuing telemetry transport)协议通信的设备的自动发现、配置和移除.MQTT协议是一种基于TCP的发布订阅协议, 在物联网通信中使用较多.设备接入HA时, 每个设备只需按照HA指定的格式配置其MQTT通信模块, HA即可间接从MQTT代理获得配置信息并完成配置流程.若设备需要移除, 则它可以更新状态信息将自己移除, 也可以由HA根据超时设置自动移除.因此, HA提供实现G2的基础, SSRules需要主动与HA交互真正达到G2.

● 高自由度的输入

HA的规则输入语言为Trigger-Condition-Action(即Event-State→Event)范式, 单规则中可以含有多触发器、多动作.动作不仅可以是与设备相关的服务调用, 也可以是自定义的事件触发和状态值写入、HTTP接口调用等, 自由度很高.但是HA的自动化规则的编写非常繁琐, 用户难以使用其描述有优先级的功能需求, 并且用户自行推理编写极易遗漏或写错.此外, 由于HA的实体状态和服务调用之间的松耦合, HA提供运行时异常检查极其有限.HA在G1, G3和G4方面较弱, 因此, 这也是SSRules要重点解决的问题.

2.3 SSRules系统总体架构

SSRules系统总体架构如图 1所示.整个系统通过HA提供的接口与智能家居设备连接, 包括通过MQTT代理连接智能家居真实设备或模拟器.系统由离线的转译器子系统和在线的SSRules运行时子系统组成: 前者提供终端用户输入的SS规则到HA规则的转译, 后者提供HA抽象信息的获取和规则执行的有效性检查.SSRules引入Entity-Capability抽象(见第2.4节)来描述智能家居系统所能管控的设备(实体)及可管控的内容(能力), 用户输入的SS规则最终被SSRules转化为HA规则注入到HA的配置文件并得以执行.

● 抽象信息获取

SSRules需要HA中的实体、状态、服务的抽象信息用于SS规则的转译和异常检测, 这些信息由SSRules运行时子系统的抽象信息获取模块来提取和更新.该模块定期从HA更新实体信息并检测变化情况, 获取设备的动态信息(加入或离开), 生成SSRules所需的最新实体-能力抽象信息和动作翻译信息.

● 规则转换流程

SSRules的用户交互模块根据实体-能力抽象信息将用户输入规则所需的信息以用户友好的方式呈现在前端界面中.用户完成编辑后, 用户交互模块根据用户的输入生成SS规则文件.接着, SSRules运行时系统会调用可离线运行的转译器将SS规则转译成HA规则, 再将其更新到HA的automations.yml中.

● 异常检测设计

当由SS规则翻译得到HA规则并开始执行之后, 规则执行有效性检查模块会从HA获取所关心的状态变化事件, 定期获取全部实体的状态, 检查实体状态及其状态变化是否符合SS规则的描述, 并将因网络/设备故障等问题导致的设备状态与SS规则描述不相符等情况进行告警以及写入日志.

2.4 Entity-Capability抽象

一个智能家居系统所管理的设备可以包括真实物理设备(如空调)、虚拟设备(如天气、时钟等), 还可以是人.SSRules系统使用实体-能力抽象(entity-capability abstraction)来描述智能家居系统中各种设备的可感知和/或可控制的能力, 记为$W = \{ {\mathcal{E}_1},{\mathcal{E}_2},...,{\mathcal{E}_{{N_D}}}\} $, N_D为实体总数.每个设备抽象为一个实体$\mathcal{E}$(entity), 每个实体由其ID e、一组能力$\mathbb{C}$(capability)以及描述各能力状态之间转移关系的状态机M组成, 即$\mathcal{E}$=(e, $\mathbb{C} $, M).

● 能力

每种能力表示单个可变化的只读或者可控属性.表 4列出了几种常见智能家居设备及其能力.每种能力可表示为一个四元组(c, k, ro, $\mathcal{J}$), 其中: c是该能力在实体内的唯一标识; k表示该能力的状态值类型, 可以是二值(binary)/多值(set)/实数(numeric)等类型之一(实数可以细分成子界类型或实数区间等, 本文为简便起见不作区分); 布尔量ro为真表示能力是只读的、为假表示是可控的; $\mathcal{J}$表示一组关联的命令序列, 其中每个元素是要执行的命令代号.

● 状态机

每个实体的状态机由该实体每种能力c的状态机组成: M_c=(V_c, $ {\mathbb{T}_c} $), 其中, V_c是能力c的状态值集合, $ {\mathbb{T}_c} $是状态值之间的转移函数.

● 若c为只读的, 则转移函数为$ {\mathbb{T}}_{c}: {V}_{c}\stackrel{[C]}{\to }{V}_{c} $, 箭头上方的C为事件转移发生的必要条件, 表示能力c仅在C为真时才可能从源状态值转移到目的状态值;

● 若c为可控的, 则转移函数的类型为$ {\mathbb{T}}_{c}: {V}_{c}\stackrel{[C]\mathcal{J}}{\to }{V}_{c} $, 箭头上方的C为动作转移允许发生的充分必要条件; $\mathcal{J}$为要执行的命令代号, 表示能力c仅在C为真时才能够接受代号为$\mathcal{J}$的动作, 或者在出现外部事件时(如用户通过遥控器、手机APP、物理开关等控制), 使得从源状态值转移到目的状态值.

在缺省的M_c中, 任意两个状态值之间存在条件为True的转移(即无条件状态转移); 若c可控, 则存在无条件动作, 它可触发任意两个状态值之间的状态转移.SSRules系统会提供初始的M_c配置文件, 其中提供部分常用设备能力及其状态转移描述, 用户也可以根据需要添加某个设备或者某一类设备的M_c补充信息.

根据c的M_c抽象, 可以进一步检测动作的执行前提, 或者判断事件的可能性.例如, 假设电扇和咖啡机的能力状态机如图 2所示: ①电扇的c₂(风速)只有在其c₁(开关)的取值为开时才可以接受改变风速的动作; ②咖啡机的咖啡状态仅在咖啡机的c₁(开关)取值为开时才能从未准备好进入准备好状态.

3 SSRules编程范式及其到HA规则的翻译

本节首先分析以状态触发器-状态动作(SS)风格设计SSRules编程范式的可行性; 然后给出SSRules提供给终端用户使用的SS规则范式的定义, 分析它在应对表 2所列的10种TAP缺陷的能力; 接着分析转译器面对的主要问题, 并引入EE中间范式作为SS规则到HA规则转换的桥梁; 最后介绍SS到EE转译的关键算法.

3.1 SS范式的引入

由第1节可知: 终端用户不太能区分事件和状态, 并且用户使用State-State时序范式会比使用含Event触发器的范式更易写对规则.为此, 我们以状态为基础, 通过规则分组、自动优先级等改进措施(详见第3.2节)来提供“State-trigger State-action”编程范式, 简称SS范式.

● SS范式的易写易改性

SS范式可以较为简洁地表达用户日常常见需求; 并且和Event-State→Event相比, SS范式写出的规则容易随需求的变更和细化进行修改.为了更清晰地表述这两种范式的区别, 表 5给出了分别用两种范式描述夜灯开关的规则, 其中, 模式是HA提供的虚拟传感器, 有回家模式和离家模式两种取值.在SS范式下, 作用于夜灯的3条规则均作为子句按序置于“ FOR夜灯”语句中, 每个子句形如“EXPECT A [WHILE B]”, 表示当B成立(或永真)时, 期望A中各能力为指定的值; 对于同一实体的多个EXPECT, SSRules按从前往后以第一个WHILE条件成立的EXPECT子句所指定的期望状态为准.然而, 当用Event-State→Event表示时, 为了正确表达所列出的几种情况的状态保持和它们之间的转移关系, 需要写出9条规则来细分情况.假设用户用SS范式先写了后2条规则, 运转一段时间后他又添加第1条保证离家模式下夜灯总是关闭的需求, 在SS范式下, 这种添加是简单的; 但是若使用Event-State→Event达到相同目的, 则需要在原先第3条~第6条、第8条、第9条这6条规则基础之上新增3条规则, 并修改原先的规则细节(修改部分用粗体字表示), 这样的编写和修改非常琐碎、易错.

● SS范式的局限

SS范式能表达大多数智能家居的场景需求, 但是无法表达无状态或者难以抽象出状态的事件和动作(如无状态按钮、记录日志等).对于这类需求, 目前仍需编写Event-State→Event规则.因此, SSRules将SS范式转译为Event-State→Event, 并允许两种范式共存.未来可以扩展降低这类需求编程难度的具体范式.

3.2 SS范式的定义

表 6的左部列出了SSRules系统支持的SS范式的抽象语法, 其中: FOR语句集结同一动作实体的所有规则, 且约定组内靠前的规则优先级更高; 每条规则(ssrule)包含在WHILE子句指定的条件成立时, 对该实体全部或部分能力的期望状态; 多条规则按从前到后的次序、以第1条满足WHILE条件的规则中的EXPECT子句来设置期望的实体能力状态; 一般地, 无WHILE子句的规则放在最后作为安全默认.Condition中的“entityID. capName op value”, “historyOp timeperiod entityID.capName value”分别表示当前状态和历史状态型原子判断, 其中, 历史状态运算符historyOp的4种可能取值的含义举例如下.

●   “WITHIN 5分钟电扇.开关关”表示电扇的开关在5分钟内曾经处于关闭状态, 则该原子判断为真;

●   “!WITHIN 5分钟电扇.开关关”表示电扇的开关在5分钟内不曾处于关闭状态, 则该原子判断为真;

●   “STAY 5分钟电扇.开关开”表示电扇的开关在5分钟内持续处于开启状态, 则该原子判断为真;

●   “!STAY 5分钟电扇.开关关”表示电扇的开关在5分钟内未一直处于开启状态, 则该原子判断为真.

3.3 SS范式的缺陷避免能力分析

SS范式天然地排除了表 2中所列的缺陷⑨、缺陷⑩这两种缺陷.对于在使用State-State时序范式时可能存在的缺陷①~缺陷⑧这8种缺陷, SS范式的表示机制能完全避免缺陷①优先级冲突; SS范式的表示及转译机制能部分解决或消除缺陷②安全默认偏差、缺陷③非瞬时动作、缺陷⑥重复触发, 其附带效果可以辅助改善缺陷④缺少反向动作; 对于缺陷⑤无限循环、缺陷⑦不确定时序等缺陷的检测, 可以通过模型检查等方法在规则转译之前避免; 由于难以提供通用的鉴别何谓矛盾的机制, 因而SSRules不能解决缺陷⑧矛盾的动作.下面分别讨论SS范式应对缺陷①~缺陷③和缺陷⑥的措施.

(1) “按动作实体将规则分组、组内规则有序”可完全避免缺陷①优先级冲突

用户只需移动规则在组内的相对位置, 免除显式设置优先级数值的困难.由于同一动作实体的各规则优先级不同, 故无缺陷①(示例见3.1节).

(2) “将配置的安全默认规则自动作为动作实体的最低优先级规则”可辅助消除缺陷②安全默认偏差

SSRules提供可配的安全默认设置文件, 其中的条目形如“实体/实体类ssrule”可描述指定实体或实体类的默认期望状态, SSRules会自动将其追加到相应实体的规则集尾部, 作为最低优先级规则.例如针对门锁可以配置默认安全规则“EXPECT (状态, 锁定)”, 则用户只需描述其他需求, 如:

    FOR门锁EXPECT (状态, 未锁定) WHILE人体传感器.状态==激活[AND其他安全条件]

而SSRules会自动在尾部追加“EXPECT (状态, 锁定)”.只要人体传感器不再激活, SSRules就会按最后一条无条件子句的期望状态将门锁锁定.这种做法消除缺陷②的前提是要正确配置安全默认文件.

如果用户希望在人体传感器激活后2分钟内均保持门锁解锁, 可使用SS范式提供的历史状态判断:

FOR门锁EXPECT (状态, 未锁定) WHILE WITHIN 2分钟人体传感器.状态激活[AND其他安全条件]

(3) “通过避免用户直接编写动作”可避免缺陷③非瞬时动作和缺陷⑥重复触发

在SSRules中, 状态转移所需要的动作的执行前提被描述在实体-能力抽象信息中, 用户只能选择期望的状态, 而无法写出有缺陷的程序造成对非瞬时动作的多次触发动作而进入不期望的状态.例如: 针对冲泡咖啡这样的非瞬时动作, 如果主人希望每天7:00让咖啡机工作, 且咖啡机工作完成后自动关闭, 7:00~7:20之外的时间不开启咖啡机, 则用SS范式编写的规则为:

FOR咖啡机

EXPECT (开关, 开) WHILE时钟.时间 > 7:00 AND时钟.时间 < 7:20 AND咖啡机.咖啡状态==未准备好

EXPECT (开关, 关)

当咖啡机开启后, 即使咖啡未准备好, SSRules转译后的HA规则也保证不会再出现开启动作.而用户倘若用State-State→Event范式, 容易写出如下有缺陷的规则, 造成咖啡机多次启动:

             IF咖啡未准备好AND时间处于7:00~7:20之间THEN启动咖啡机

对于重复触发缺陷, 能够用SS范式表达的规则可以用上述类似的机制来避免; 而不能够用SS范式表达的规则, 仍需要使用Event-State→Event或者Event-Event→Event范式来写(未来将对此提供更直观的编程方式).

3.4 转译器面对的问题及EE中间范式的引入

● 转译器面对的问题

如果要在一个仅支持Event-State→Event范式的智能家居系统上实现对SS范式规则的支持, 需要将智能家居系统状态之间的转移和状态转移带来的新的状态设定与智能家居系统所支持的事件和动作关联起来, 并且要尽可能避免重复触发、非瞬时动作等缺陷.这一翻译过程应该对用户不可见, 是由系统自动完成的.此外, 为了从翻译的主要算法中排除HA规则描述的琐碎细节, 以及让算法一般化以支持到其他平台的移植, SSRules引入了EE中间范式(基于Event-State→Event).从而: 转译器的第1阶段, SS→EE的翻译可以避开HA的语法及实现细节, 重点是基于同一套实体-能力抽象将SS范式表示的功能需求转化为EE范式所表示的具体做法; 而第2阶段, EE→HA的翻译则只需从较为抽象的EE规则根据HA的事件/条件描述方式、动作对应表, 生成HA所需的规则细节即可.

● EE中间范式

表 6的右部列出了SSRules系统转译中使用的EE中间范式的抽象语法, 其主要特点为: 一条规则可以含有多个触发事件(event)、条件过滤(condition)和多个按顺序执行的动作(eeAction).event包括状态值变化事件“entityID.capName FROM range TO range”和状态保持事件“entityID.capName STAYON value REACH timeperiod”: 前者表示给定实体能力的取值从一个值集变迁到另一个值集, 后者表示指定的实体能力保持给定值value的时间长达timeperiod时触发该事件.目前, SSRules仅对二值类型的能力提供状态保持事件.EE范式中条件过滤condition的定义与SS范式一样.

● EE规则到HA规则的转译

EE规则到HA规则的翻译是一一对应的, EE规则的状态值变化事件可以对应到HA的state_changed事件和在HA规则的condition中对事件数据中的old_state和new_state的限制条件.EE规则中的状态保持事件可以转译为在HA中的延时执行和自定义事件触发.EE规则中的条件表达式可以对应到HA条件表达式中的相同树形结构.EE规则中, 实体能力的取值对应到HA规则中的状态对象state或者状态对象attribute中的附加状态; EE规则中, 对实体能力的历史状态判断被对应到HA规则中的自定义状态对象取值判断; EE规则中的一个或多个动作被单个或组合对应到HA中无参或带参的服务调用.

3.5 SS规则集与EE规则集的符号表示与一些定义

为了方便后文的说明和理解, 我们引入表 7中的符号以及几个基本概念, 这些符号和表 6定义的语法结构一一对应.例如: G^S对应于语法定义中的一个ssrulesGroup, R^S对应于一个ssrule, R^S中的C和$\mathcal{X}$分别对应于WHILE子句中的条件表达式和EXPECT子句中的期望状态组.wt和st分别表示“WITHIN”和“STAY”.

对于一个由N_D个实体组成的智能家居系统$ W = \{ {\mathbb{E}_1},{\mathbb{E}_2},{\mathbb{E}_{{N_D}}}\} $, 每个$ {\mathbb{\dot{E}}_i} $由三元组(e, $\mathbb{C}$, M)描述.在某个时刻下, W的系统状态记为σ, 它是各实体的各能力到状态值的映射, 即σ(e, c)表示实体e的能力c在该时刻的状态值.不论是SS范式的程序$\mathbb{G}$^S, 还是EE范式的程序$\mathbb{R}$^E, 都是对系统状态变迁的描述; 而转译的目标是由$\mathbb{G}$^S得到$\mathbb{R}$^E, 使得$\mathbb{G}$^S与$\mathbb{R}$^E满足一致性.在定义一致性之前, 我们先定义系统抽象状态ω, 然后定义SS规则与系统抽象状态ω的关系, 包括规则在ω下是否激活、规则是否与ω兼容.

定义1(系统抽象状态). 对于规则引擎来说, 系统当前状态σ、当前时刻τ_now以及状态变化轨迹$\mathbb{T}$可抽象为一个三元组ω=(σ, τ_now, $\mathbb{T}$), 称之为系统抽象状态.其中, $\mathbb{T}$=((e₁, c₁, v₁, τ₁), ,…, (e_n, c_n, v_n, τ_n)), (e_i, c_i, v_i, τ_i)表示实体e_i的能力c_i在τ_i时刻变为v_i(i∈{1, …, n}), 它只记录状态值发生变化的特定实体的特定能力及其新状态.状态变化可能由外部事件引起(如用户交互、环境变化), 也可能由$\mathbb{G}$^S或$\mathbb{R}$^E执行动作序列引起.每当发生状态变迁时, 都相当于$\mathbb{T}$更新为$\mathbb{T}$⊎(e_n+1, c_n+1, v_n+1, τ_n+1), 其中, τ_n+1为状态变迁发生时的τ_now.

定义2(规则在系统抽象状态ω下激活). 假设G^S=(e, $\mathbb{R}$^S)为某动作实体e的SS规则组, $\mathbb{R}_\mathcal{X}^S$表示$\mathbb{R}$^S中期望状态组均为$\mathcal{X}$的规则子集, 当前的系统抽象状态为ω.称期望状态组相同的一组规则$\mathbb{R}_\mathcal{X}^S$在ω下激活, 是指该组内任意一条规则R^S激活; 而规则R^S在ω下激活, 是指在该规则所在的规则组G^S内, 其前面的规则的条件(对应WHILE子句, 即C)在ω下都未满足, 而该规则的条件R^S.C满足.

定义3(规则与系统抽象状态ω兼容). 规则R^S与系统抽象状态ω不兼容, 是指在ω下R^S激活且R^S.$\mathcal{X}$尚不成立; 而R^S与ω兼容, 是指在ω下R^S未激活或者R^S.$\mathcal{X}$已成立; 一组规则与ω兼容, 是指组内每条规则与ω都是兼容的; 一组规则与ω不兼容, 是指组内存在与ω不兼容的规则.

实际的规则引擎提供的时间戳的精度是有限的.假设系统抽象状态ω中的时间戳都有最小时间单位(例如1秒), τ_now以最小时间单位离散地更新.那么, 对于规则集合执行方式的假设如下.

● SS规则执行假设.假设无时序缺陷的规则组$\mathbb{G}$^S的执行方式为: 每当发生状态变化, 或者τ_now变为新值之后, 判断$\mathbb{G}$^S中是否存在与最新的ω不兼容的规则.如果存在这样的规则R^S, 说明其对应实体e不满足R^S的期望状态组$\mathcal{X}$, 于是计算e上的需要执行的动作序列$\mathbb{A}$, 使得$\mathbb{A}$执行后实体e的状态符合$\mathcal{X}$;

● EE规则执行假设.假设无时序缺陷的规则组Ρ^E的执行的方式为: 设$\mathbb{R}$^E中的所有触发事件可分为状态变化事件E^I和状态保持事件E^H这两种类型, 每当出现与E^I相符的状态变迁, 或者每当τ_now的更新触发了E^H中的某个状态保持事件后, 检查与触发事件相符的各条规则.如果存在R^E, R^S.C在ω下成立, 则执行$\mathbb{R}$^E.$\mathbb{A}$.

定义4(SS与EE的一致性). 称$\mathbb{G}$^S与$\mathbb{R}$^E一致是指: 对于无时序缺陷的$\mathbb{G}$^S, $\mathbb{R}$^E, 在上述规则执行假设下(且不存在超时、执行失败、规则重叠执行的情形), 从与$\mathbb{G}$^S兼容的任意系统抽象状态ω开始, 对于同样的、同时刻的、一次发生一个事件的外部事件序列, $\mathbb{G}$^S所产生的状态变迁序列和Ρ^E所产生的状态变迁序列一致.

与$\mathbb{G}$^S一致的$\mathbb{R}$^E不唯一, 原因在于: ① $\mathbb{R}$^E中不会被执行的规则不影响一致性; ②一个条件较弱的EE规则(如一条规则$R_1^E$, 条件$R_1^E.C$为时钟.状态==白天)可等价于多个条件更强的EE规则(如等价于规则$R_2^E$和$R_3^E$, 条件$R_2^E.C$和$R_3^E.C$分别为“时钟.状态==白天AND模式.状态==回家模式”和“时钟.状态==白天AND模式.状态==离家模式”); ③一条EE规则R^E还可以等价于m条EE规则$R_i^E(i = 1,...,m)$, 满足${R^E}.\mathbb{E} = { \cup _i}R_i^E.\mathbb{E}$; ④逻辑表达式有多种等价表述.

3.6 SS规则到EE规则的转译

图 3详细说明了SS规则到EE规则的转译算法实现, 其中: 图 3(a)中的算法1是总控算法; 图 3(b)是相应的流程图, 转译器的输入分别是左上角的实体-能力抽象信息W和右上角的SS规则集合$\mathbb{G}$^S, 输出是与输入SS规则集对应的EE规则集$\mathbb{R}$^E(右下角).

转译的具体流程为:

● SS规则集解析器首先会解析用户输入的$\mathbb{G}$^S, 并将解析结果传给动作序列信息生成模块;

● 然后, 动作序列信息生成模块会将同一动作实体e的SS规则序列G^S=(e, $\mathbb{R}$^S)按照EXPECT子句作用的期望状态组分类, 期望状态组$\mathcal{X}$相同的SS规则组$\mathbb{R}_\mathcal{X}^S$中的多条规则会放在一起处理: 一方面, 调用ConditionalActionsPairs(e, $\mathcal{X}$, W)(见算法2), 计算实体e上所有可能的动作序列$\mathbb{A}$_j和每种动作序列的执行前提C_j, 得到二元组集合$ Pair{s_\mathcal{X}} = \{ ({C_j},{\mathbb{A}_j})|j \in \{ 1,n\} \} $; 另一方面, 求出与规则组$\mathbb{R}_\mathcal{X}^S$不兼容的条件${\mathit{\Psi} _\mathcal{X}}$(见算法1第5行), 这是事件发生后、动作执行前系统抽象状态所应满足的条件;

● 接下来, 事件筛选模块首先调用CandidateEvents(${\mathit{\Psi}_\mathcal{X}}$, W)(见算法3), 根据${\mathit{\Psi}_\mathcal{X}}$生成一组候选事件Ε(这些事件可能对${\mathit{\Psi}_\mathcal{X}}$的成立与否有影响); 然后, 对Ε中的每个事件E调用ShouldRejectEvent(E, ${\mathit{\Psi}_\mathcal{X}}$, W)(见算法4), 依据缺省的事件筛选策略$\mathcal{P}$_default判断该事件是否要排除掉, 即: 若E发生后${\mathit{\Psi}_\mathcal{X}}$不成立, 则需将E排除;

● 筛选后的事件集$ \mathbb{\dot{E}}{'}$与$ Pair{s_\mathcal{X}} $一并送至EE中间表示生成模块处理, 该模块对$ Pair{s_\mathcal{X}} $中的每个元组(C_j, $\mathbb{A}$_j)调用SameActionRules($\mathbb{\dot{E}}{'},{\mathit{\Psi}_\mathcal{X}},{C_j},{\mathbb{A}_j},W$)(见算法5), 产生动作序列为$\mathbb{A}$_j的EE规则集; 然后, 经过规则合并、可读性化简后(见算法1第13行), 这些EE规则集再由EE规则集生成器汇总输出精简的EE规则集, 最终实现从SS规则得到对应的EE规则.

在转译过程中, 有多个环节需要与Z3交互: 在转译开始之前, 转译器会根据实体-能力抽象构建Z3数据类型和Z3常量, 并将对应关系填入Z3-Python数据结构转换模块中的Z3常量映射表; 在转译过程中, 事件筛选模块和EE中间表示生成模块通过Z3判定事件的可满足性; 规则合并模块通过Z3判断等价的条件部分, 合并触发事件; 可读性化简模块通过Z3进行表达式化简以减少条件表达式长度.

下面结合算法2~算法5详细介绍动作序列信息生成、事件筛选以及EE中间表示生成这3个关键模块.

算法2. “执行前提-动作序列”对集合的生成(ConditionalActionsPairs).

输入: 实体e, 期望状态组$\mathcal{X}$, 系统实体-能力抽象W;

输出: 结构如{(C₁, $\mathbb{A}$₁), …, (C_n, $\mathbb{A}$_n)}的Pairs, 表示实体e满足C_i时要达到$\mathcal{X}$需执行$\mathbb{A}$_i.

1. Pairs=Ø, $ {\mathbb{C}_\mathcal{X}} = \mathcal{X}{|_c} $   //$\mathcal{X}$|_c表示对$\mathcal{X}$中的(c, v)二元组集合的c投影得到实体能力集合

2. if $\exists \mathit{\boldsymbol{c}} \in {\mathbb{C}_\mathcal{X}}$, c不是可控能力then error

3. ${\mathbb{C}'_\mathcal{X}} = Reorder({\mathbb{C}_\mathcal{X}},\{ {M_\mathit{\boldsymbol{c}}}|\mathit{\boldsymbol{c}} \in {\mathbb{C}_\mathcal{X}}\} )$

4. for each c_i in ${\mathbb{C}'_\mathcal{X}}$, (c_i, v_i)∈$\mathcal{X}$ (i=1, …, m) do

5.     $Set{s_i} = SplitRangeByAction({M_{{\mathit{\boldsymbol{c}}_i}}},{v_i})$   //将c_i的状态值域${V_{{\mathit{\boldsymbol{c}}_i}}}$根据${\mathbb{T}_{{\mathit{\boldsymbol{c}}_i}}}$和目标值v_i划分为$\{ V_1^i,...,V_{{k_i}}^i\} $

6. end for

7. for Sets₁×Sets₂×…×Sets_m中的每一个组合$(V_{{j_1}}^1,...,V_{{j_m}}^m)$ do   //考察每一种初始取值的组合

8.      $\mathbb{A} = CheckedActionSteps(({\mathit{\boldsymbol{c}}_1},V_{{j_1}}^1,{v_1}),...,({\mathit{\boldsymbol{c}}_m},V_{{j_m}}^m,{v_m}))$   //返回动作序列或特殊值IMPOSSIBLE

9.      $C = AsCond({\mathit{\boldsymbol{c}}_1},V_{{j_1}}^1){\text{ and}}...{\text{and }}AsCond({\mathit{\boldsymbol{c}}_m},V_{{j_m}}^m)$   //c₁~c_m的取值范围分别处于$V_{{j_1}}^1,...,V_{{j_m}}^m$的条件

10.      Pairs=Pairs∪{(C, $\mathbb{A}$)}

11. end for

● 动作序列信息生成模块

该模块会针对期望状态组$\mathcal{X}$相同的SS规则组$\mathbb{R}_\mathcal{X}^S$, 调用算法2产生可能的动作序列及其执行前提集合$ Pair{s_\mathcal{X}} = \{ ({C_j},{\mathbb{A}_j})|j \in \{ 1,n\} \} $, 并求出与$\mathbb{R}_\mathcal{X}^S$不兼容的条件${\mathit{\Psi}_\mathcal{X}}$(见算法1第5行).算法2的第2行指出, $\mathcal{X}$投影得到的能力集合${\mathbb{C}_\mathcal{X}}$中的每个能力都必须是可控的.如第2.4节所述, 可控能力c的状态机M_c=(V_c, $\mathbb{T}$_c)中的转移函数$ {\mathbb{T}}_{c}: {V}_{c}\stackrel{[C]\mathcal{J}}{\to }{V}_{c} $, 每个状态转移带有条件C以及要执行的命令$\mathcal{J}$, C中可能会涉及其他实体能力.考虑到实际需求以及处理上的简便, 假设${\mathbb{C}_\mathcal{X}}$中各能力的状态转移条件C中依赖的其他能力遵循部分序关系, 算法2的第3行调用Reorder函数将${\mathbb{C}_\mathcal{X}}$中的能力按这种序关系重排得到${\mathbb{C}'_\mathcal{X}}$, 这样在第8行就可以尝试按此顺序依次检查动作转移的可行性.另外, 对于${\mathbb{C}'_\mathcal{X}}$中的能力c_i, 其状态值域${V_{{\mathit{\boldsymbol{c}}_i}}}$可能是无限的实数, 而${M_{{\mathit{\boldsymbol{c}}_i}}}$是有限的, 故第5行的SplitRangeByAction函数会检查${M_{{\mathit{\boldsymbol{c}}_i}}}$中到达期望值v_i的各个状态转移动作$\mathcal{J}$和转移条件C, 将$\mathcal{J}$, C相同的状态转移的起始状态涉及的各状态值划分到同一个子集, 从而形成${V_{{\mathit{\boldsymbol{c}}_i}}}$的有限子集划分Sets_i, 进而可能减少第7行要处理的${\mathbb{C}'_\mathcal{X}}$初始状态情形的数目, 也能够减少后续规则合并的运算次数.

下面结合图 4的例子来解释.该例子的动作实体为“电扇”, 有3条SS规则.这些规则按期望状态组$\mathcal{X}$是否相同分成两组$ {\mathbb{R}}_{{\mathcal{X}}_{1}}^{S}(①③)和{\mathbb{R}}_{{\mathcal{X}}_{2}}^{S}(②) $.以$\mathbb{R}_{{\mathcal{X}_2}}^S$组为例, 根据该组的$\mathcal{X}$₂“(开关, 开)(风速, 低)”和图 2电扇的状态机, 按照算法2求出到达$\mathcal{X}$₂的所有执行前提-动作序列对(图 4左下方的4种动作序列).另一方面, 该模块也要输出$\mathbb{R}_{{\mathcal{X}_2}}^S$不兼容的条件${\mathit{\Psi}_{{\mathcal{X}_2}}}$用于稍后的事件筛选, ${\mathit{\Psi}_{{\mathcal{X}_2}}} = $模式.状态==回家模式AND温湿度传感器.温度 > 28℃ AND (电扇.开关!=开OR电扇.风速!=低).

● 事件筛选模块

该模块先使用算法3生成候选事件, 接着进一步使用算法4, 根据系统可能的状态变迁对事件进行筛选.算法3主要根据一个执行前要满足的条件C生成候选事件集, 旨在以较低运算成本快速得到较小的待筛选事件集.其中: 第2行分别获取C中出现的实体能力集合ECs以及原子条件集合C_atom, 原子条件有当前状态判断(e, c, O, v)和历史状态判断(e, c, O_h, t, v)这两种形式(如表 7); 第4行的SplitRangeByCond则是根据C_atom对实体Ε的能力c的状态值域V_c进行划分, 将对所有原子条件的判断影响一致的状态取值划分到同一个子集, 从而将实数类型的事件转移转化为了有限情形; 第5行~第7行分别产生状态变化事件E^l和状态保持事件E^H, 能够涵盖C中出现的原子条件取值变化的情形.对于历史状态原子条件(e, c, O_h, t, v), 由于只支持二值类型的能力c, 在固定e, c, t下, O_h和v最多有8种组合, 我们为之按v的两种取值产生2种状态保持事件, 忽略O_h; 而被忽略的O_h仍在C中, 传递到后续由算法5产生的EE规则R^E=(Ε, C, $\mathbb{A}$)中.这种状态保持事件E^H能在状态迁移中快速知道实体能力保持状态的时长, 再结合C中的O_h进行状态保持的可满足性检查.

算法3. 候选事件生成算法(CandidateEvents).

输入: 条件表达式C, 系统实体-能力抽象W;

输出: 包含所有可能使C的值变化的事件集合Ε.

1. Ε=Ø

2. ECs=C|_{(e, c)}; C_atom=AtomFormulas(C)

3. for each (e, c) in ECs, 由W得c的值域V_c do

4.      Sets=SplitRangByCond(e, c, V_c, C_atom)   //划分值域V_c

5.       Ε=Ε∪{(e, c, V₁, V₂)|∀V₁, V₂∈Sets, V₁≠V₂}

6.       T={t|(e, c, O_h, t, v)∈C_atom}   //C中原子条件涉及对c的时长t的要求

7.       Ε=Ε∪{(e, c, v, t)|∀v∈V_c, ∀t∈T}

8. end for

算法4. 事件排除判定算法(ShouldRejectEvent).

输入: 事件E, 事件发生后应为真的条件Ψ,

实体-能力抽象W, 事件筛选策略$\mathcal{P}$=$\mathcal{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 = SysStateAsser{t_\mathcal{P}}(E,!\mathit{\Psi},\mathit{\Psi},{C_E})$

    //$\mathcal{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).

输入: 筛选后的事件集Ε′, 不兼容条件${\mathit{\Psi}_\mathcal{X}}$, 动作序列$\mathbb{A}$_j, 执行前提C_j, 系统实体-能力抽象W;

输出: 与动作序列$\mathbb{A}$_j相同的规则集合$\mathbb{R}_\mathbb{A}^E$.

1. if $\mathbb{A}$_j 为空序列then return

2. $\mathbb{R}_\mathbb{A}^E = \emptyset $

3. for each E in $\mathbb{\dot{E}}'$ do

4.      C_E=E形如(e, c, V_s, V_d)?EventCond(M_c, V_s, V_d): True

5.      $ C={\mathit{\Psi}}_{\mathcal{X}}\text{ and }{C}_{j}{|}_{ Postcond(E)} $   //在事件E发生后, ${\mathit{\Psi}_\mathcal{X}}$ and C_j成立的条件

6.      $Assertion = SysStateAsser{t_\mathcal{P}}(E,!\mathit{\Psi},C,{C_E})$   //默认策略仍假设事件发生前!Ψ为真

7.      if Z3.Satisfiable(Assertion, W)=“UNSAT” then continue

8.      if $\mathbb{A}$_j=“IMPOSSIBLE” then error “无法保证翻译规则的一致性”

9.      $\mathbb{R}_\mathbb{A}^E = \mathbb{R}_\mathbb{A}^E \cup (\{ E\} ,C,{\mathbb{A}_j})$

10. end for

算法4旨在判断事件E可否发生并在发生后使得Ψ($\mathbb{R}_\mathcal{X}^S$不兼容的条件)为真(进而导致Ψ对应的某个动作序列的执行), 需要根据筛选策略$\mathcal{P}$做关于系统抽象状态的可满足性判定.筛选策略从保守到激进有多种策略: 激进的策略需要对事件发生之前的系统状态做出更强的假设, 而保守的策略只需要相对较弱、能够更快判定的假设.本文提出的默认策略$\mathcal{P}$_default为: 事件发生前Ψ为假($\mathbb{R}_\mathcal{X}^S$兼容), 事件发生后Ψ为真($\mathbb{R}_\mathcal{X}^S$不兼容), 且事件发生前后V_s→V_d的事件转移条件C_E成立, 则该事件不会被排除.

继续以图 4的规则组$\mathbb{R}_{{\mathcal{X}_2}}^S$为例, 其不兼容条件为${\mathit{\Psi}_{{\mathcal{X}_2}}}$.对于事件E=(模式, 状态, {离家模式}, {回家模式}), 由于M_模式状态的离家模式到回家模式的转移没有必要条件, 故C_E=TRUE.按照默认筛选策略, 将模式.状态在事件发生前后的值分别代入$!{\mathit{\Psi}_{{\mathcal{X}_2}}}$和${\mathit{\Psi}_{{\mathcal{X}_2}}}$, 则Assertion为“!(离家模式=回家模式AND温湿度传感器.温度 > 28℃ AND (电扇.开关!=开OR电扇.风速!=低)) AND (回家模式=回家模式AND温湿度传感器.温度 > 28℃ AND (电扇.开关!=开OR电扇.风速!=低))”.这一断言是可满足的, 所以事件E不被排除, 将交由EE中间表示生成处理.

以图 4中$\mathbb{R}_{{\mathcal{X}_1}}^S$规则组为例, 本文的默认事件筛选策略与系统抽象状态的可能转移之间的联系如图 5, 左上方是以G^S中的若干规则组的状态为局部视角时系统抽象状态的转移图, 按照一次一个外部事件、一次执行一条规则的系统执行假设, 不会发生的系统抽象状态转移用点线表示.按照当前默认的事件筛选策略$\mathcal{P}$_default, 认为可能到达$\mathbb{R}_{{\mathcal{X}_1}}^S$的不兼容状态的状态转移由右上图中4条深色的系统抽象状态转移边表示(与左上图对比, 边③是在当前系统抽象和规则执行假设下不会发生的状态转移), 但是在左下方粗粒度的系统抽象状态转移图上, 却对应着相同的转移边.使用较保守的事件筛选策略的缺点就在于可能未排除边③这样的边, 进而存在生成出不能执行到的规则的可能性.需要注意的是: EE规则中的事件和图中的系统抽象状态转移边不一定一一对应, 能够触发同一条EE规则的所有可能的状态转移在细粒度的状态转移图上可能对应多条边.例如EE规则“IF模式.状态FROM {回家模式} TO {离家模式} WHILE电扇.开关==开THEN电扇.开关关闭”, 该规则被触发的情况可能是图 5右上图中的状态转移①, 也可能是状态转移②.从这一角度来说, 使用较保守的事件筛选策略的优点在于判定条件较少, 运算更快(判定的是宽泛的系统抽象状态集合间的转移).

● EE中间表示生成模块

该模块调用算法5生成EE规则.以上一步骤筛选输出的事件E=(模式, 状态, {离家模式}, {回家模式})、规则组$\mathbb{R}_{{\mathcal{X}_2}}^S$的不兼容条件${\mathit{\Psi}_{{\mathcal{X}_2}}}$为例, 对于图 4左下方中的4个执行前提-动作序列对, 都要判断执行前提是否可能满足并生成规则.这里以4对中的左上一对为例, 由算法5的第5行得到的条件: “回家模式=回家模式AND温湿度传感器.温度 > 28℃ AND (电扇.开关!=开OR电扇.风速!=低) AND (电扇.开关!=开AND电扇.风速!=低)”作为动作执行的完整前提条件, 同时也应当是E发生后为真的条件, 结合事件发生前应当为真的条件!Ψ, 得到关于系统状态的断言并判定是可满足的, 因此生成一条规则:

    IF模式.状态FROM {离家模式} TO {回家模式} WHILE温湿度传感器.温度 > 28℃ AND

        电扇.开关!=开AND电扇.风速!=低THEN电扇.开关打开, 电扇.风速设定低.

算法4虽然和这里的算法5都需要对一组系统状态的断言做可满足性求解, 但是算法4不考虑动作序列的执行前提, 其筛选结果能够被同一$\mathcal{X}$的多个动作序列复用; 且能够通过算法4筛选的只有较少数量事件, 这些事件至少能够与一个动作序列组合成为规则.算法4的存在, 减少了转译过程中总的可满足性判定的次数.若直接将候选事件集合与多种动作序列的组合输入算法5, 可能需要较多次数的不必要的求解.

4 方法评估

为了验证SSRules的系统设计的有效性, 基于Python开发了SSRules运行时子系统和离线转译器; 基于Javascript开发了SSRules前端用户交互模块, 方便终端用户设置SS规则(如图 6左上方); 同时, 结合已有用户调查^[15]构建智能家居使用情景, 在这些场景下, 就SSRules系统运行情况和规则转译效果进行评估和讨论.

4.1 智能家居实验场景搭建

为了能够评估SSRules, 需要将一些设备连接到HA, 并让设备和环境产生足够多的状态转移, 以覆盖各种可能的使用情形.但是, 使用真实设备无法在短时间得到这样的测试场景并且调试不便.为此, 我们基于Unity游戏引擎开发了一个能接入HA的智能家居模拟器HA-Simulator(其界面如图 6下方).利用HA-Simulator可以将时间加速, 以较高的速度发生系统的状态变化, 并对温湿度/烟雾浓度等环境因素合理建模.这使得在短时间内测试大量的智能家居系统状态变迁并验证SSRules成为可能.

在HA-Simulator中模拟了12种智能家居设备, 布局和类型如图 6右上方所示, 这些设备通过HA的MQTT Discovery集成方式接入HA.此外, 在HA中以自定义方式提供模式、天气和时钟这3种虚拟设备.在模拟器中, 同一房间内的设备受同一组环境变量(温度、湿度、烟雾浓度)的影响.模拟器可以设置环境变量改变的速度, 进而间接改变虚拟传感器的取值; 同时, 模拟器中的设备可以被手动调节或者由模糊测试程序随机改变.

4.2 实验结果分析

● SS→HA翻译对比

首先参考以往用户调查^[15]中用户的智能家居需求, 构造了10组SS规则作为测试集, 其中: 编号为1~6的规则组不含历史状态, 编号为T1~T4的规则组含有历史状态.每一组规则至少有一个动作实体(设备), 规则中会引用多个相关实体的状态.另外, 规则组6、规则组T3、规则组T4含有多个动作实体.按照当前的事件筛选策略, 翻译前后的规则条数比较见表 8.最终生成的HA规则条数均多于SS规则条数, 比例为2倍~4倍.

● HA规则运行覆盖率

在由SS转译得到HA规则之后, 每一组HA规则均在模拟器上运行20分钟.除第1组规则(包含空调与温湿度传感器)和第3组规则(包含排气扇以及其他4个相关实体)之外, 其余组的HA规则均全部被执行过.这说明SS→HA转译器为其余8组规则产生的HA规则集中没有多余的规则, 当前的事件筛选策略对于多数测试样例是比较合理的.对于含有多余规则的情形, 而第1组的4条SS规则为:

FOR客厅空调

EXPECT (模式, 制冷)(温度, 18℃) WHILE客厅温湿度传感器.温度 > 28℃

EXPECT (模式, 制热)(温度, 20℃) WHILE客厅温湿度传感器.温度 < 10℃

EXPECT (模式, 干燥) WHILE客厅空调.模式!=制热AND客厅空调.模式!=制冷AND客厅温湿度传感器.湿度 > 65%

EXPECT (模式, 关) WHILE客厅温湿度传感器.温度 < 22℃ AND客厅温湿度传感器.温度 > 14℃

而在转译出的13条HA规则中, 没有被执行过的(可能是多余的)一条HA规则用EE范式表达为:

    IF客厅温湿度传感器.温度FROM (-30℃, 10℃)∪(28℃, 70℃) TO [10℃, 28℃] WHILE

        客厅空调.模式!=制冷AND客厅空调.模式!=制热AND客厅空调.模式!=干燥

            AND客厅温湿度传感器.湿度 > 65% THEN客厅空调.模式设定干燥

原因在于: 当前的筛选策略没有假设系统状态在事件发生之前的瞬间与整个规则组G^S的描述相符, 而仅仅假设系统状态与第3条SS规则的描述是兼容的(即第3条规则未激活或者其期望状态已满足).但是在测试运行中, 当温度低于10℃或者高于28℃时, 系统状态持续与G^S的描述相符, 空调模式一定是制热(第2条SS规则激活)或者制冷(第1条SS规则激活), 所以该条EE规则是多余的, 通过使用更激进的事件筛选策略可将其消除.

● HA规则运行异常检测

表 8的后3列分别是在20分钟的随机测试下, 各组的HA规则的执行次数、异常检测模块发现的异常次数(系统状态不满足动作实体的SS规则集合中激活的那一条SS规则的期望状态)与总检测次数之比、是否存在连续两次检测到异常的情况.各组总的规则执行次数相差不大.异常检测模块目前以定时轮询方式实现, 在20分钟内进行了1 200次异常检查, 未发现连续出现异常的情形.对于单次检测出现异常的情况, 经过查看记录的状态日志和HA规则的执行序列, 这些异常均因网络延迟(动作执行不及时)造成.

5 相关工作

智能家居目前在市场上受到了广泛欢迎, 越来越多的家庭配置了智能家居的设备.智能家居最吸引人的功能之一就是以应用程序的形式支持自定义自动化.但是由于用户未经过专业的培训, 导致其自定义的规则存在一定的缺陷, 甚至无法定制规则, 这引起了人们对物联网增强生活的风险的担忧.这些风险远非仅仅是学术上的, 更紧迫的是对用户的生命财产的威胁.Triger-Action编程(TAP)是一种流行的终端用户编程方式, 可以让用户实现其智能设备和云服务的交互.然而, 用户有时并不能通过TAP正确表达自己的意图并实现相应的功能.随着此类系统部署在越来越复杂的智慧家居场景中, 用户必须能够识别编程错误并解决.

为了给终端用户提供更高效的服务, 首先需要理解用户编程出现错误和规则冲突的原因.Huang等人^[6]认为, 现有TAP编程系统(如IFTTT)的过分简化限制了程序的表达能力.提出了改进IFTTT界面的建议, 以减轻因心理模型不正确而引起的问题.Corno等人^[28]认为: 现有的TAP接口界面暴露了太多功能, 并迫使用户在众多混乱的网格菜单中进行搜索, 导致用户无法得到原本需要的功能.为此, 作者提出了EUDoptimizer, 旨在以交互方式协助终端用户使用循环中的优化器来组合IF-THEN规则, 减少了编写Triger-Action规则所需的工作. Brackenbury等人^[17]提出了10类常见的TAP编程错误类型, 作者发现: 错误的存在, 使参与者更难正确预测规则的行为.Davidoff等人^[29]发现, 智能家居用户的日常活动与编程任务并不匹配.论文描述了家庭想要的控制, 并提出了有助于终端用户编程系统实现这种控制的7种设计原则.Brush等人^[20]认为: 为使智能家居得到更广泛的使用, 需要解决成本高昂、设备不灵活、客观理性差和安全保障这4个障碍.论文还为进一步研究提供了几个方向, 包括消除变化结构的需要、为用户提供简单的安全原语并支持家庭设备的组合.

因此, 为减少终端用户编程的错误, TAP平台需要对用户生成TAP规则进行指导, 并实现模型的检查, 自动发现规则漏洞或冲突.Wang等人^[14]利用IFTTT平台, 探讨了在Triger-Action平台中可能存在的规则漏洞, 并借助于自然语言处理的方法推断Triger-Action信息, 实现了一个模型检查系统iRuler, 用于发现物联网中的规则间漏洞.Celik等人^{[19, 30, 31]}认为, 物联网中存在大量的设备交互.因此, 不仅需要验证单个设备, 还需要对设备的联合行为进行检查.Soteria^[30]是一种静态分析系统, 可从IoT应用程序的源代码中提取状态模型, 并通过模型检查来验证IoT应用程序或IoT环境是否符合已标识的属性.考虑到静态分析在估计物联网状态转换方面的局限性, Celik等人^[19]继续开发了一个动态分析系统IoTGuard, 可通过在运行时监视设备执行行为, 来强制执行已标识的属性, 并可以通过阻止违反属性的设备操作, 或在运行时要求用户批准或拒绝违规操作来应对属性违规.肖丁等人提出的基于知识图谱的KGIID算法^[32]能够检测TAP编程模型中冲突的动作(隐式冲突).孟岩等人提出的HODETECT检测工具^[33]利用无线侧信道技术从智能家居应用中提取工作逻辑, 并用有限状态自动机建模, 通过在应用运行时监听无线加密流量的元数据来推测应用的执行状态, 间接检测恶意应用.陈星等人^[34]提出了智能家居情境感知服务的运行时建模与执行方法, 能够降低开发者开发智能家居情境感知服务的难度和复杂度.

更进一步地, TAP服务提供平台还需要对存在缺陷的规则进行修复.Nandi等人^[26]注意到, 终端用户在编写规则时所犯的一个常见错误是触发器数量不足.因此, 作者开发了TrigGen, 它可以根据规则中的操作自动生成一组必要和充分的触发器, 来帮助终端用户正确地编写规则.这种做法在一定程度上减少了意外行为和安全漏洞的发生率, 但是其对于潜在冲突的检测还有提升空间.为帮助非专业的物联网用户系统地实现高置信度的实时HA-IoT系统, Bu等人^[16]介绍了一种自动化端到端编程辅助框架MenShen, 它能够检查自动化规则集是否违反规范, 从而为用户提供可能的解决方案.Zave等人^[24]建议在运行时通过优先级来减少设备管理和交互的成本, 并通过组合机制实现了目标.Zhang等人^[15]将用户需要表达的属性转换为线性时序逻辑(LTL), 自动合成满足属性的TAP规则, 并修复现有的TAP规则.

6 总结

基于规则的智能家居系统是目前流行的一种智能家居系统, 而编写琐碎、修改困难、错误难以追踪是以往用户调查^[15]所反映的问题.本文提出的SS范式以及配套的SSRules系统实现方式, 使得用户规则编写和修改的复杂程度大为减低; 同时, 设计的SS规则到HA规则的转译算法使得输入的SS规则能够在现有的智能家居系统HA规则引擎上运行, 并且通过辅助的SSRules运行时模块, 能够提供规则执行异常检测的能力.

未来的工作重点在以下两个方面: 一方面, 采用模型检测技术实现对SS范式无法避免的缺陷进行检测, 并设计辅助用户编写SS规则和避免缺陷的实时反馈算法; 另一方面, 对于SS范式目前不能够表达的需求, 进行用户调查并寻找合适的多范式协同输入对策.