智能家居平台构件适应与协同模型及形式化分析

李爱萍，马俊伟，段利国

(太原理工大学 计算机科学与技术学院,太原 030024)



智能家居平台构件适应与协同模型及形式化分析

李爱萍，马俊伟，段利国

(太原理工大学 计算机科学与技术学院,太原 030024)

摘要:以解决智能家居平台运行过程中的构件适应与协同问题为目的，保证设备独立性与数据一致性为特点，提出一种基于构件适应与协同的智能家居平台逻辑模型,对平台及各构件进行形式化描述与建模,并结合平台功能需求对模型性质进行分析与验证。实验表明,在本模型下平台构件的适应与协同满足不死锁、不中止、不发散的必要性质,且在并行处理多用户请求的条件下能够实现数据一致性与操作有效性。本研究对智能家居平台的研发与验证有一定意义。

关键词:智能家居平台;构件适应;构件协同;形式化

智能家居平台是针对智能家居设备管理的软件开发框架[1-2]。一般定义智能设备及控制程序的访问接口、协议及控制方法,将家庭看作一个智能家居设备的集合,通过家庭、房间、区域的概念把这些设备有机地组合起来。在对设备的控制上,硬件设备被定义成提供一个或者多个服务的单元,而这些服务可以被第三方控制程序发现和调用[2-3]。

构件适应是软件工程中的一个关键问题[4-5],是指将部分满足要求的构件按照合适的适应结构组装在一起,形成满足用户需求的复合构件。智能家居平台需要将智能设备、控制程序、操作系统等构件复合成为用户提供服务的综合系统,各构件的适应与协同就显得至关重要。而目前国内外在该领域的研究工作较少,且缺乏基于严谨数学基础的形式化研究支持,导致平台构件适应协同等问题无法进行有效验证,大大阻碍了智能家居行业的创新与发展。

以解决平台运行过程中的构件适应与协同问题为目的,保证设备独立性与数据一致性为特点,提出一种基于构件适应与协同的智能家居平台逻辑模型,对构件及平台进行形式化描述与建模,并结合平台功能需求对模型性质进行分析与验证,证明了模型的正确性与实用性。

1相关工作

文献[10]设计了一种智能家居系统规则冲突避免和冲突检测的方法,它将场景中的用户、触发器、环境实体和执行器这四个部分抽取出来,建立UTEA (User-Trigger-Environment-Actuator)形式化的模型;进而定义了多种规则关系和冲突模型,最后设计了冲突检测算法。但并未对系统本身的性质进行研究,且尚未实现对系统其它关键性质如数据一致性等问题的分析验证。

文献[11]提出一个智能家居上下文模型,根据智能家居系统自身的需求和上下文感知工作流框架的特点,采用FollowMe框架进行智能家居平台设计。可在系统投入运行之前对系统的正确性进行验证,发现系统潜在的漏洞,避免系统投入运行后发生严重的错误。然而验证过程结构复杂,容易出现错误信号甚至冲突,导致验证可靠性大打折扣。

文献[12-13]分别提出了基于ZigBee和Android平台的智能家居系统。研究重点皆为功能的丰富和性能的优化,并未对系统可靠性、并行处理性质等作出分析,其实验结果难以令人信服。

2智能家居平台逻辑模型

智能家居平台的实际系统结构包括感知层、传输层及应用层等[14],本文仅研究应用层上各构件的适应与协同,并以此为目的建立逻辑模型进行形式化分析与验证。

智能家居平台的逻辑模型如图1所示,分为四类构件。

1) 控制程序(Control App)。即用户使用的第三方应用,它从操作系统的数据容器中获知当前智能设备的状态,并通过智能家居开发框架所提供的接口来对智能设备进行控制。

2) 设备控制框架(Accessories Controlling Frameworks)。设备控制框架是智能家居平台的核心部分,它定义实现智能家居管理的类、关系和方法,实现控制程序对智能设备的控制。操作系统(Operating System)是控制框架的载体,框架方法的实现可能需要调用操作系统的相关接口。另外,实现对设备的控制应至少需要以下两个大类，

a.Home表示一个独立的房屋,不同的房屋需要分别进行控制。一个房屋可能由多个用户进行管理,并存在多个房间(Room),设备可以被附属在Room中,用户通过Room找到智能设备,进行单个或统一通信和配置。

b.AccessoryOb表示房屋中一个独立的智能设备。一个智能设备有且仅有一个AccessoryOb对象与其对应。一个AccessoryOb对象提供一个或多个服务(service),每个Service有多个属性(characteristics)来表示其状态。

3) 数据容器(Common Database)。数据容器是操作系统中用于保持数据一致性的数据存储器。智能设备的状态信息被存储在Common Database中,所有控制程序都须从此获得设备信息。

4) 智能设备(Accessory)。即所要控制的智能设备硬件。

图1　智能家居平台逻辑模型Fig.1　Logical Model of Frameworks for Smart Home

3智能家居平台及构件的形式化描述

借鉴文献[5]的描述方法,智能家居平台中每个构件的形式化描述规则如下。

式中：D是所有输入值的集合;R是所有输出值的集合;I(x)表示所有前置条件,每一个前置条件定义了构件的合法输入,只有前置条件被满足时相应服务才能被执行(前置条件是在提供服务之前对象状态的约束);O(x,y) 表示所有后置条件,即提供服务后所得到的所有状态的集合(后置条件是在提供服务之后对象状态的约束),每一个后置条件定义了一个合法输入所对应的所有合法输出。例如:

Component(inxseq, outyN, outzN)

prex≠Null

post1y∈elements(x) ∧(∀e∈elements(x)|y≥e)

post2z∈elements(x) ∧(∀e∈elements(x)|y≤e)式中：符号‘in’ 代表输入参数;符号 ‘out’ 代表输出参数; ‘seq’ 和 ‘N’ 表示参数类型;‘pre’ 代表前置条件,描述了构件的所有合法输入;‘post1’ 和‘post2’ 代表后置条件,描述了构件所有的合法输出。

3.1构件形式化模型

3.1.1控制程序构件

ControlApps(in Room seq,in Acc seq,in Ser seq,in Cha seq,in Cmd seq,out Room seq, out Acc seq, out Req seq)

pre1Room ∈ elements (rooms)

pre2Acc∈(elements (accessories,rooms)∧(rooms==Room))

pre3Ser∈(elements (services, accessories)∧ (accessories==Acc))

pre4Cha∈(elements (characteristics, services) ∧ (services=Ser))

pre5Cmd∈(elements (commands, rooms,accessories) ∧ (rooms==Room)∧ (accessories==Acc))

post1Req∈(elements (requests, rooms, accessories, commands)∧ (rooms==Room) ∧ (accessories==Acc) ∧ (commands==Cmd))

控制程序构件的输入参数为房间(Room)、设备(Acc)、服务(Ser)、属性(Cha)和命令(Cmd),输出为同一房间、设备及用于控制程序和设备控制框架进行协同的命令(Req)。前置条件为Room属于房间集合elements(rooms)中的元素,Acc属于当rooms值等于Room时二元组elements(accessories, rooms)中的元素,其他前置条件的表示方法与含义与其类似。后置条件为Req属于在Room、Acc、Cmd为确定值时四元组elements (requests, rooms, accessories, commands)中的元素。

其他构件的形式化描述方法与含义与该构件相类似。

3.1.2设备控制框架构件

该构件的输入构件有控制程序及智能设备两个,且其中一个为输入时,另一个为输出。因此需要表示为两个部分。

输入为控制程序时:

OS1(in Room seq, in Acc seq, in Req seq, out Ctrl seq)

pre1Room∈elements (rooms)

pre2Acc∈(elements (accessories, rooms) ∧ (rooms==Room))

pre3Req∈(elements (requests, rooms, accessories)∧ (rooms==Room) ∧ (accessories==Acc))

postCtrl∈(elements (controls, rooms, accessories, requests)∧ (rooms==Room) ∧ (accessories==Acc) ∧ (requests==Req))

其中Ctrl是用于设备控制框架与智能设备进行协同的命令。

输入为智能设备时:

OS2(in Ser2 seq,in Cha2 seq, out Room2 seq, out Acc2 seq,out Ser2 seq, out Cha2 seq)

pre1Ser2∈(elements (services, accessories)∧ (accessories=Acc)) ⨁Ser2==null

pre2Cha2∈(elements (characteristics, services)∧ (services=Ser2)) ⨁Cha2==null

post1Room2∈elements (rooms)⨁Room2==null

post2Acc2∈(elements (accessories, rooms)∧ (room=Room2)) ⨁Acc2==null

post3Ser2∈(elements (services, accessories)∧ (accessories=Acc2)) ⨁Ser2==null

post4Cha2∈(elements (characteristics, services)∧ (services=Ser2)) ⨁Cha2==null

3.1.3智能设备构件

Accessory(in Ctrl seq, out Ser2 seq, out Cha2 seq)

preCtrl∈(elements (controls, rooms, accessories)∧ (rooms==Room) ∧ (accessories==Acc))

post1Ser2∈(elements (services, accessories)∧ (accessories=Acc)) ⨁Ser2==null

post2Cha2∈(elements (characteristics, services)∧ (services=Ser2)) ⨁Cha2==null

3.1.4数据容器构件

Database(in Room2, in Acc2 seq, in Ser2 seq, in Cha2 seq, out Room3 seq, out Acc3 seq, out Ser3 seq, out Cha3 seq)

pre1Room2∈elements (rooms)

pre2Acc2∈(elements (accessories, rooms) ∧ (rooms==Room2))

pre3Ser2∈(elements (services, accessories)∧ (accessories==Acc2))

pre4Cha2∈(elements (characteristics, services) ∧ (services=Ser2))

post1Room3∈elements (rooms)

post2Acc3∈(elements (accessories, rooms) ∧ (rooms==Room3))

post3Ser3∈(elements (services, accessories)∧ (accessories==Acc3))

post4Cha3∈(elements (characteristics, services) ∧ (services=Ser3))

数据容器存储从设备控制框架输入的房间和设备信息并进行更新,同时提供控制程序需要的房间设备信息。

3.2智能家居平台形式化模型

在平台系统各构件模型已确立的基础上,按照复合构件构造规则[4]对各构件进行复合,得出智能家居平台构件适应与协同的整体系统模型。

模型为循环结构,执行过程为:

System=ControlApps+OS1+Accessory+OS2+Database+System*

式中：符号‘+’表示构件的顺序执行关系,执行语义是依次执行ControlApps、OS1、Accessory、OS2 、Database五个构件,最后再次执行System；*表示0或多次的重复,用于表示平台对智能设备的多次控制。

智能家居平台整体模型形式化描述如下:

System (in room seq, in acc seq, in ser seq, in cha seq, in cmd seq, out room’ seq, out acc’ seq, out ser’ seq, out cha’ seq)

pre1Room∈elements (rooms)

pre2Acc∈(elements (accessories, rooms) ∧ (rooms==Room))

pre3Ser∈(elements (services, accessories)∧ (accessories==Acc))

pre4Cha∈(elements (characteristics, services) ∧ (services=Ser’))

pre5Cmd∈(elements (commands, rooms, accessories) ∧ (rooms==Room)∧ (accessories==Acc))

post1∃Req∈(elements (requests, rooms, accessories, commands)∧ (rooms==Room) ∧ (accessories==Acc) ∧ (commands==Cmd))

post2∃Ctrl∈(elements (controls, rooms, accessories, requests)∧ (rooms==Room) ∧ (accessories==Acc) ∧ (requests==Req))

post3Room’∈elements (rooms)⨁Room’==null

post4Acc’∈(elements (accessories, rooms)∧ (room=Room’)) ⨁Acc’==null

post5Ser’∈(elements (services, accessories)∧ (accessories=Acc’)) ⨁Ser’==null

post6Cha’∈(elements (characteristics, services)∧ (services=Ser’)) ⨁Cha’==null

4模型应用实验

智能家居平台应使用户能够在搭载平台的操作系统上通过应用程序控制和配置智能设备,主要实现以下四大功能[3]:

1) 房间设置。用户能够创建、命名、调整以及删除虚拟的房间及房间组合。

2) 用户管理。具有相关权限的用户能够对当前连接在同一家庭中的其他用户进行管理。

3) 设备的增加与删减。用户可以便捷地发现设备并将其添加到相应房间中,也可以快捷地删除设备。

4) 情景设置。用户可以对多个设备进行配置,并将其定义为一个“情景”,从而通过对“情景”的控制来方便地调配多个智能设备。

4.1构件协同模型建模

应用实验以本文提出的形式化模型为基础,模拟在智能家居平台模型上并发进行各类功能操作的过程,来检验构件协同性质以及并行处理性质。模拟工具为形式化进程分析工具PAT平台,使用语言为CSP#。

为保持数据一致性,对数据容器和智能设备的任何操作都需要互斥进行[15]。因此,以经典算法面包店算法[16]作为各进程访问以上资源的互斥算法,并表示为进程Cs()。在组成智能家居系统的过程中,构件之间需要进行适应连接及工作协同,而在实际运行过程中则表现为通过协议进行通信交互。整个过程的形式化表示中会涉及构件间的多个通信协议,为增强模型易读性,直接以协议名称表示通信事件。

4.1.1房间设置功能过程建模

对该功能所要完成的任务进行分析,用户首先通过Cs()进程从数据容器中获知房间当前情况,随后发出配置请求事件requestA。实现对Room的控制。HomeDelegate协议实现从应用程序到平台的通信。homeoperateR事件表示对请求进行的处理,最后调用Cs()在Common Database中写入最新配置信息,同时通过协议将结果返回用户程序。该功能行为流程用CSP#建模表示为:

SetupHome()=Cs();requestA-> HomeDelegate-> homeoperateR-> Cs(); HomeDelegate-> Skip

4.1.2用户管理功能行为流程表示

用户通过Cs()获取当前用户信息,随后发出用户管理请求requestB。用户信息由Home模块进行处理,因此通过HomeDelegate协议进行传达。HomeoprateU表示Home模块收到指令后对用户进行操作,最后调用Cs()更新信息,同时使用协议将处理结果返回用户。该功能行为流程用CSP#建模表示为:

ManageUsers()=Cs();requestB->HomeDelegate-> homeoprateU-> Cs();HomeDelegate-> Skip

4.1.3设备增删功能行为流程表示

用户调用Cs()后发出设备增删请求requestC,通过HomeDelegate协议与Home模块协同,通过homeoprateB操作增删设备。最后通过Cs()更新信息并通过AccessoryDelegate协议告知用户结果。该功能行为流程用CSP#建模表示为:

AddandRemovingAccessories()=Cs(); requestC-> (HomeDelegate-> homeoprateB-> Cs();AccessoryDelegate-> Skip

4.1.4情景设置功能行为流程表示

用户在设置情景时是对多个家居设备进行配置,但彼此之间是互相独立的。为简化模型,减少系统状态数,将此功能的行为流程模拟为对单个设备的配置,最后通过声明多个该过程模型来达到模拟情景设置的情况。首先用户仍然是通过Cs()获得设备当前的设置,然后发出操作指令requestD,通过HomeDelegate协议传递至AccessoryOb模块。accoperate事件表示模块在进行相关处理,处理后通过预定义的协议CommunicateDelegate与设备进行通信。随后设备根据命令进行操作,表示为事件accessoyconf,最后通过callback事件返回结果。由于设备是临界资源,故从accoperate事件到callback事件为原子操作,在CSP#中用atomic{}进行表示。最后调用Cs()将更改后的设备信息写入数据容器并通过AccessoryDelegate协议告知用户结果。该功能行为流程用CSP#建模表示为:

DefScenes()=Cs(); requestD-> HomeDelegate-> atomic {accoperate->CommunicateDelegate-> accessoryconf-> callback-> Skip};Cs();AccessoryDelegate-> Skip

综上,智能家居平台所实现的四大功能流程CSP#建模已完成。对于一个用户,其通过平台对智能家居在家庭中进行配置的所有操作就包含于以上四个功能之中。因此,以一个user()进程表示一个用户的行为,该用户在某一时间所做的操作为以上功能之一。用CSP#表示为:

User(i)=SetupHome() [] ManageUsers() [] AddandRemovingAccessories() [] DefScenes()

其中参数i为用户编号。

最后,模拟N个用户同时通过智能家居平台来配置智能家居作为整个系统的进程System()。

System()=|||m:{0..N-1} @ User(m)

4.2模型性质的分析与验证

实验从构件协同性质和并行处理性质两方面进行分析与验证。

4.2.1构件有效适应与协同的性质验证

在协同性质方面,该行为流程模型所涉及的构件适应与协同应具备不死锁、不中止、不发散的性质[17]。用CSP#断言可表示为:

#assert System() deadlockfree;

#assert System() divergencefree;

#assert System() nonterminating.

通过PAT平台对流程模型进行自动验证,可以得出构件的适应与协同具备相关性质。

4.2.2模型并行处理性质验证

本验证通过LTL线性时序逻辑[18]验证对模型并行处理多用户请求时的数据一致性与操作有效性进行验证。具体来说:第一,数据容器作为临界资源,不能同时有大于一个的用户对其进行访问;第二,在情景设置功能中成功对设备状态进行更改才能达到目的,因此需要验证requestD指令发生后是否总能发生accessoyconf事件;第三,为保证数据一致性,每个用户进行使用任一功能时都需要访问两次Common Database,在读取一次数据后必须还有一次写入操作。第四,为确保Common Database中的数据正确表示对应家居设备的情况,需要验证数据返回后、写入Common Database之前,是否有其他事件更改设备数据。在PAT中相关语句和表示为:

#define collision (count> 1);

#assert System() |=collision;

#assert System() |=requestD-> []<>accessoryconf;

#assert User() |=ncs->[]<>ncs;

#assert User() |=callback-> Skip->[]ncs

在以上五条语句中,首先将用于记录临界区用户数的count参数大于1的情况定义为collision事件,然后声明断言验证System()是否有collision事件出现。若没有,即验证不通过,则说明临界资源不存在用户数大于1的情况;第三条表示在System()中若发生requestD事件,则接下来必发生accessoryconf事件;第四条中ncs事件为互斥算法中的第一个事件,一个User()中发生两次该事件则说明其访问量两次Common Database,完成了读和写的操作;第五条表示发生callback事件且原子操作结束后(Skip),下一个事件是否始终为ncs;若不是,则说明存在其它事件修改数据的潜在风险。

同样地,使用PAT平台对流程模型的并行处理性质进行LTL检测,从结果可以得出模型具有所要验证的性质。

将本文所提模型的验证结果与第二节中的相关工作进行比较,可得以下优点:

1) 实现了控制器与智能设备的相对独立。在本模型中,控制程序与智能设备通过操作系统进行协同,两者相互独立。两个部分的开发者只需遵从系统提供的接口即可进行开发,实现了软件和硬件端的相对独立设计与操作。

2) 解决了构件协同中的数据一致性难题。本模型中的数据都储存在数据容器中,所有操作都需要在其中读取或写入数据,保证了对设备进行操作的有效性和安全性等。

3) 实现了设备的联动操作。由于设备被安排在房间中,因此可以以房间为单位进行从属设备的统一设置与联动操作,亦可以以情境为前提进行多个设备的设定。真正实现智能地为用户服务,而不是单一、复杂地操作设备。

5结论

提出一种基于构件适应与协同的智能家居平台逻辑模型,对平台及各构件进行了形式化描述与建模,并结合平台功能需求对模型性质进行了分析与验证。实验表明,在本模型下平台构件的适应与协同过程满足不死锁、不中止、不发散的必要性质,且在并行处理多用户请求的条件下能够实现数据一致性与操作有效性,对智能家居平台的研发与验证有一定意义。下一步的工作中将在模型中加入时钟控制,建立实时模型,更加准确地模拟系统工作状态,进一步提出平台研发与验证的意见和建议。

参考文献：

[2]APPLE,Inc.Introducing homekit[EB/OL].[2014-11-18].https:∥developer.apple.com/homekit/.

[3]APPLE,Inc.HomeKit user interface guidelines[EB/OL].[2014-11-18].https:∥developer.apple.com/homekit/ui-guidelines/.

[4]谢兄,张维石.构件适应和组装的形式化语义描述[J].计算机工程与应用,2007,43(21):36-39.

[5]MOREL B,ALEXANDER P.Aslicingapproach for parallel component adaptation technical report ITTC-FY2003-TR-29120-01[R].Information and Telecommunications Technology Center,University of Kansas,2002.

[6]SUN Jun,LIU Yang,SONG Jin,et al.Modeling and verifying hierarchical real-time systems using stateful timed CSP[J].The ACM Transactions on Software Engineering and Methodology,2013,22(1):1-29.

[7]LIU Yang.User Manual[EB/OL].[2013-05-17].http:∥pat.sce.ntu.edu.sg/wp-source/resources/OnlineHelp/htm/index.htm.

[8]SUN Jun,LIU Yang，DONG Jinsong.Model checking CSP revisited:introducing a process analysis toolkit[C]∥MARGARIA T,STEFFEN B.The Third International Symposium on Leveraging Applications of Formal Methods,Verification and Validation,Porto Sani,Greece.Berlin Heidelberg:Springer,2008:307-322.

[9]SUN Jun,LIU Yang,DONG Jinsong,et al.PAT:towards flexible verification under fairness[C]∥BOUAJJANI A,MALER O.The 21th International Conference on Computer Aided Verification (CAV 2009).Grenoble,France,2009,5643:709-714.

[10]王栩凯.智能家居系统规则冲突检测机制的研究与实现[D].北京邮电大学,2015.

[11]张星.基于Petri网的智能家居原型系统的设计与分析[D].华东理工大学,2013.

[12]庞泳,李光明.基于ZigBee的智能家居系统改进研究[J]. 计算机工程与设计,2014,35(5):1547-1550.

[13]陈玮,秦会斌,曹曙光,等.基于Android平台的智能家居系统设计[J].电子技术应用,2015,41(10):158-160.

[14]韩江洪.智能家居系统与技术[M].合肥:合肥工业大学出版社,2005.

[15]张协衍,章兢.基于连续时间模型的多智能体系统采样数据一致性[J].自动化学报,2014,40(11):2549-2555.

[16]LAMPORT,LESLIE.The mutual exclusion problem has been solved[J].Communications of the Association for Computing Machinery,1991,34(1):110-119.

[17]谢开斌,陈海明,崔莉,等.物联网软件体系结构中的感执模型的求精[J].软件学报,2014(8):1659-1670.

[18]Gerth R,Peled D,Vardi M Y,et al.Simple on-the-fly automatic verification of linear temporal logic[J].Simple On-the-fly Automatic Verification of Linear Temporal Logic-ResearchGate,1995:3-18.

(编辑：朱倩)

The Formal Analysis of Component Adaptation and Interaction of Frameworks for Smart Home

LI Aiping，MA Junwei，DUAN Liguo

(CollegeofComputerScienceandTechnology,TaiyuanUniversityofTechnology,Taiyuan030024，China)

Abstract:This paper proposed a smart home frameworks model concentrated on components’ adaptation and interaction.Formal description and modeling of frameworks and components were performed.According to the functional requirements,the properties of the model were analyzed and verified.Experimental results show that adaptation and interaction of components have the essential qualities of being deadlock-free, divergence-free and nonterminating.And the model can keep data consistency and operational effectiveness under the condition of processing user requests in parallel.The modeling and verification methods have certain significance in the formal verification and research of smart home frameworks.

Key words:sart home frameworks;component adaptation;component interaction;formal methods

文章编号:1007-9432(2016)02-0212-06

*收稿日期：2015-05-30

基金项目：山西省科技攻关资助项目(工业):遗留软件再工程的研究与实现(20120321030)；太原理工大学校科技发展基金资助项目(2012L067)

作者简介：李爱萍(1974-)，女，山西文水人，博士，副教授，主要从事计算机应用，软件形式化描述与验证，软件体系结构等的研究，(E-mail)tyutli@163.com

中图分类号:TP399

文献标识码:A

DOI：10.16355/j.cnki.issn1007-9432tyut.2016.02.017