物联网系统时间自动机建模的研究与应用

陈 光 蒋同海 王 蒙 唐新余 季文飞

1(中国科学院新疆理化技术研究所 新疆 乌鲁木齐 830011)2(中国科学院大学 北京 100049)3(江苏中科西北星信息科技有限公司 江苏 无锡 214135)4(新疆民族语音语言信息处理实验室 新疆 乌鲁木齐 830011)5(中国科学院物联网研究发展中心 江苏 无锡 214135)

0 引 言

物联网(Internet of Things,IoT)，指的是将各种信息传感设备通过多种组网技术与互联网相结合形成的动态松耦合系统[1]。物联网是继计算机、互联网与移动通信网络之后的世界信息产业的第三次浪潮。国内外业界人士都将发展物联网视为新的技术创新点和经济增长点[2-5]。从总体上看，我国的物联网技术产业链仍处于概念和探索阶段，物联网的整个技术体系架构和产业模式尚未成熟[6]。

与传统互联网不同，物联网被认为具有一些特殊的性质[1]。物联网的特殊性质使得物联网系统相比于一般的互联网系统具有更多的系统状态，并且因为这些系统状态之间的转换与物理世界的交互性，往往具有很强的实时性要求[7]，所以需要在物联网系统设计阶段进行充分的考虑。

时间自动机可以直观地刻画实时系统与时间有关的行为[8]，是物联网实时系统进行设计和建模的重要方法。基于时间自动机的理论研究，也产生了许多时间自动机建模和模型检测工具[9]。

本文探讨了基于时间自动机进行物联网系统建模的理论、方法、工具和建模实践。以物联网温度传感器感知物理温度环境为例，说明了基于时间自动机理论使用UPPAAL建模工具进行物联网系统建模和模型检测的方法，并进行了温度感知的建模实践。

1 相关工作

在时间自动机的理论研究方面，文献[10-12]都对时间自动机的形式化理论进行了研究。文献[12]最早认为时间自动机是一个4元组的概念。韩德帅等[11]在关于时间自动机的理论研究中认为时间自动机是6元组的概念，但是没有在约束集合的定义中考虑时间自动机的属性变量和属性约束。李力行等[10]在基于时间自动机的建模与验证研究中，考虑到了时间自动机中的属性约束对时间自动机格局造成的影响，提出了7元组的时间自动机形式化定义，但是对于时钟约束和属性约束的区别和联系，阐述得不够明确。上述研究中，都没有指出如何依据时间自动机理论进行时间自动机建模的方法，也没有说明时间自动机理论与建模实践之间的关系。

本文基于Bengtsson等[12]的时间自动机理论研究(UPPAAL以此为基础实现)，结合使用UPPAAL进行时间自动机的建模实践，总结得出了时间自动机的6元组形式化定义。给出了时钟变量、时钟约束、属性变量、属性约束，以及时钟属性映射(时钟属性解释)与时钟属性映射满足时钟属性约束等相关概念的精确形式化定义。本文结合一个建模实例说明了时间自动机理论研究对于建模的指导意义。基于这些理论研究，说明了使用时间自动机建立物联网系统模型的方法。

在使用时间自动机进行建模和模型检测方面，文献[13-14]对机器人系统和关键通信节点进行了时间自动机的建模和分析；文献[15]将时间自动机建模和模型检测的方法应用到高铁跨界临时限速的问题上，但是都没有给出明确的建模过程和检测方法；文献[16]对RFID等常见的物联网物端传感设备进行了时间自动机建模和分析，但是没有将其与物联网云端服务联动起来，对完整的物联网业务系统进行建模。上述所有的建模研究更侧重于在理想情况中对物联网系统进行建模，没有对可能出现的故障情况做出考虑，在系统组成的建模上也没有体现出如何针对系统容错性进行建模。

本文在第5节的建模实践中，根据物联网温度传感器感知物理环境温度的需求，建立了物联网实时温度感知系统模型。对物联网系统可能出现设备故障的情况以及系统容错性做出了充分的考虑。通过设计，所有接入到这个物联网系统中的温度传感器都可以进入故障状态，并设定，只要有一个温度传感器没有发生故障，则温度传感器管理服务就不会进入故障状态，以此体现所设计物联网系统的容错性。即使在系统中接入了发生故障的传感器，甚至不接入传感器，温度传感器管理服务也可以快速指示出现故障的状态，以此体现物联网实时系统的实时感知特性。

2 时间自动机建模理论

时间自动机的建模和验证方法都是建立在时间自动机的理论上实现的。本节首先介绍与时间自动机形式化定义相关的概念，探讨关于时钟和属性约束之间的关系。然后给出时间自动机的形式化定义，澄清时间自动机状态和格局的关系，并给出格局转换、紧迫和原子状态的形式化定义。最后给出时间自动机网络的形式化定义。

2.1 属性变量和属性约束

在一个时间自动机中可能存在多个属性变量，这些属性变量构成了属性变量的集合V。例如：V={temperature,humidity,luminosity}表示了一个由温度、湿度和光照度构成的属性变量集合。

属性约束可以是包含多个属性变量的元组，例如ρ=〈temperature≥10,humidity<50〉，但不一定包含所有的属性变量，例如〈luminosity≥0〉只对属性变量luminosity做出限制。

2.2 时钟变量和时钟约束

时钟约束可以是包含多个时钟变量的元组，例如：η=〈x≥2,1≤y<10,z>0〉，但不一定包含所有的时钟变量，例如〈y≥0〉只对时钟变量y做出限制。

2.3 时钟属性约束集合

2.4 不变性约束与守卫约束

时间自动机引入了位置的概念，时间自动机的所有位置组成时间自动机的位置集合N。对于N中的某个位置l，可以对应两种不同形式的约束。

定义7限制时间自动机状态可以进入某个位置l的约束称为守卫性约束(guard)，一般用g来表示。

值得注意的是，I仅包含了到不变性约束的映射，对于守卫约束不做定义和限制。

2.5 时间自动机约束之间的关系

在进行时间自动机物联网体系结构建模的时候，必须明确时钟约束与属性约束、守卫约束与不变性约束之间的关系，在设计时间自动机的约束条件时做到概念清晰。

时钟约束与属性约束可以看成是从构成约束的变量集合类型角度进行分类的结果。而守卫约束和不变性约束则是从约束与位置的关系角度进行分类的结果。在时间自动机建模的时候，这些约束可以互相包含。守卫约束或者不变性约束中既可以包含时钟约束，也可以包含属性约束。而一个时钟约束或者属性约束既可能是一个不变性约束，也有可能是一个守卫约束。

例如图1所示的时间自动机中的约束所示的时间自动机模型中，S0位置的不变性约束是时钟约束c≤10，S1位置的不变性约束是属性约束temperature<30，属性约束temperature>26和时钟约束c>10共同构成进入S1状态的守卫约束。

图1 时间自动机中的约束

2.6 时钟属性映射与满足约束

定义10时钟属性映射u满足时钟属性约束φ。对于时钟属性约束φ∈B(X)，如果时钟属性映射(时钟属性解释)u中的每一个分量〈Xi=c〉均满足时钟属性约束φ中对应分量上的约束条件，即〈Xi=c〉∈〈Xi～c〉，则称时钟属性映射(时钟属性解释)u满足时钟属性约束φ，记为：u∈φ。

对应地，时钟属性解释u满足守卫时钟约束g，可以记为：u∈g；时钟属性解释u满足不变性约束I(l)，可以记为：u∈I(l)。

可以将一个时钟属性约束〈X1～c1,X2～c2,…,Xn～cn〉理解为一个n维空间中点集的概念，而时钟属性映射(时钟属性解释)〈X1=c1,X2=c2,…，Xn=cn〉可以理解为一个具体的点的概念。这样可以很容易理解时钟属性映射满足时钟属性约束的概念，比如〈x≤2〉代表一个以2为端点的射线，因为x∈R，射线是无穷多个点的集合， 而〈x=1〉代表了一个具体的点，由于点属于点集，所以自然有〈x=1〉∈〈x≤2〉。

2.7 时间自动机的形式化定义

2.8 时间自动机的状态和格局

需要特别指出的是，各研究对时间自动机的状态定义，不相同，文献[10]认为时间自动机的状态就是指时间自动机的位置，而文献[12]认为时间自动机的状态是包含了时钟属性解释的二元组。为了避免混淆，考虑到在学术研究中探讨“时间自动机状态转换”的时候一般是指时间自动机的位置发生变化，因此我们将状态与位置的概念等同起来，引入一个新的概念——格局，用它来表示包含时间取值和属性取值的一个时间自动机状态。

定义12时间自动机的格局(Status)。一个时间自动机的格局定义为一个二元组〈l,u〉，其中l∈N代表一个位置，u代表此时间自动机时钟属性变量集合X下的一个时钟属性解释。可以理解时间自动机的格局为包含某个时钟属性解释的位置，也就是包含了时间和属性取值的状态。

定义13时间自动机格局变换(Operational Semantics)。对于时间自动机中的一般位置(状态)l∈N，包括初始状态l0都存在以下2种变换方式：

从时间自动机格局变换的定义中可以很容易推导出一个定理：在时间自动机中，属性变量取值的变化只发生在位置改变的格局变换中，时间流逝的格局变换不会造成属性变量取值的变化。

2.9 紧迫状态与原子状态

从紧迫状态和原子状态的定义中可以看出，紧迫状态(位置)和原子状态下都不包含时间流逝的格局变换。并且处于原子状态的时间自动机在进入此状态与进行位置改变的格局变换时，不能被其他的时间自动机的任何格局变换中断。

2.10 时间自动机网络

定义16时间自动机的积和时间自动机网络。对于2个时间自动机A1=〈N1,l10,Σ1,X1,E1,I1〉和A2=〈N2,l20,Σ2,X2,E2,I2〉，如果它们的消息(动作)集合满足Σ1∩Σ2≠∅，则称时间自动机A1、A2是能够串联(组装)的，将A1和A2串联的结果称为2个时间自动机的积，记为：A1‖A2。

时间自动机A1和A2的积，可以看成一个新的时间自动机，即A1‖A2=〈N1∪N2,〈l10,l20〉,Σ1∪Σ2,X1∪X2,E1∪E2,I1∪I2〉，对于新的时间自动机Ai如果也满足(Σ1∪Σ2)∩Σi≠∅，则可以继续串联时间自动机进行积的运算。

将2个或者2个以上时间自动机串联的结果M=A1‖A2‖…‖An,n≥2 称为时间自动机网络。

3 时间自动机建模方法

物联网系统的时间自动机建模主要分为2个步骤。首先针对物联网系统中的每一个资源进行时间自动机建模，然后再把不同资源的时间自动机模型，通过发送和接收消息组合起来，形成时间自动机网络。接下来我们以物理环境和温度传感器为例，探讨基于时间自动机理论进行物联网系统建模的方法。

假设对夏日的某个室内空气温度进行建模，室外温度为50 ℃，室内温度初始为40 ℃，由于室内温度低于室外温度，室内温度以每100个时间单位增长1 ℃的速度增长，直到50 ℃。室内温度可以被物联网系统中的传感器物理实体所感知，读取当前的室内温度进入物联网系统。

对于室内温度物理环境时间自动机，首先从状态上进行分析，室内空气温度会随时间而变化，但这是其属性的变化，并没有新的状态产生，因此空气只有一个状态loop，loop是空气的初始状态，后续所有属性变化也一直停留在此状态，即有：

NAir={loop}，lAir0=loop

空气能够被传感器感知其温度状态，则空气时间自动机与传感器时间自动机之间必然有消息传递，因为是感知温度，命名为GetAirTemperature，所以有：

ΣAir={GetAirTemperature}

从时钟变量和属性变量的角度分析，空气本身拥有属性温度，命名为temperature。为了模拟空气每100个时间单位增加1 ℃的性质，还应该为空气建立一个时钟计数器inc_clock，故有：

XAir={temperature,inc_clock}

为了使得温度能够在100个时间单位内完成自增，必须限制空气时间自动机停留在loop状态的时间不得超过100个时间单位。因此有：

IAir={loop→〈inc_clock≤100〉}

在传感器进行温度感知的时候，空气时间自动机无条件地将自身的温度状态发送给传感器时间自动机，因此温度感知的格局变换没有任何守卫约束与变量赋值操作，只有消息的发送：

图2 空气温度时间自动机模型

使用同样的分析方法对温度传感器进行建模，可以得到温度传感器的形式化模型：

ASensor=〈NSen,lSen0,ΣSen,XSen,ESen,ISen〉，其中：

Nsen={run,fault}，lSen0=run,

ΣSen={GetAirTemperature},

XSen={sen_clock},

ISen={run→〈sen_clock≤10〉},

对温度传感器时间自动机形式化模型进行等效转换，得到图形化的温度传感器时间自动机如图3所示。其中：“?”代表接收消息GetAirTemperature。

图3 温度传感器时间自动机模型

将建立的空气温度与温度传感器模型应用基于时间自动机的积的理论串联起来，形成时间自动机网络，就完成了一个具有简单温度感知功能的物联网系统时间自动机模型。

由于时间自动机建模分析和时间自动机形式化表述占用的篇幅过长，且形式化时间自动机表述与图形化时间自动机表述完全等效，为了节约篇幅，我们在后续的时间自动机建模讨论中，不再赘述建模分析和形式化模型表述，而直接给出图形化形式模型。但这并不意味着时间自动机理论对于建模是不重要的。事实上，时间自动机理论研究对于建立时间自动机模型具有十分重要的意义。

从时间自动机的建模方法中可以看出，物联网系统的建模过程，就是通过分析物联网系统组成资源的性质，填充其时间自动机形式化定义中所规定的内容集合，从而得到对应资源的时间自动机模型，最后再把这些物联网资源的时间自动机模型串联组装起来组成时间自动机网络，从而得到整个物联网系统的时间自动机模型。所以时间自动机理论是进行物联网系统建模的基础。

对时间自动机的形式化理论进行研究，不仅能够从数学的形式化的思维上加深对于时间自动机建模的理解，而且有助于在建模过程中对于模型中出现的概念和属性，例如时间自动机的状态和格局，时钟约束、不变性约束、守卫约束等，有清晰而深刻的认识，更有助于规范使用时间自动机进行建模的过程。在时间自动机理论的指导下使用正确的状态或者约束，刻画物联网系统资源所具有的性质，建立正确的符合客观系统资源性质和规律的时间自动机模型，从而更好地研究物联网系统在时间和状态变换方面的性质和规律，把控物联网系统设计的正确性和实时性是否满足预期的需求。

4 时间自动机建模工具

UPPAAL是由瑞典的Uppsala大学与丹麦的Aalborg大学联合研发的时间自动机建模和模型验证检测工具，主要针对实时系统的建模、仿真和性质验证。UPPAAL目前已经成功地运用于实时控制器的设计和通信协议的性质验证。

文献[8]在其研究中指出，相比于其他的时间自动机建模工具，比如HYTECH、Kronos(Grenoble)和Epsilon(Aalborg)等，UPPAAL在时间和空间上的性能明显更好，具有显著的高效性。

UPPAAL具有可视化的描述界面，使用方便、高效，实用性高。 UPPAAL设计了一个易于用户操作和使用的图形界面，主要包括三个部分：系统编辑器(system editor)、模拟器(simulator)和验证器(verifier)。

使用UPPAAL的编辑器界面进行时间自动机的建模。UPPAAL的编辑器界面如图4所示，详细的布局区域和功能菜单介绍可以参考文献[17]。

图4 UPPAAL编辑器视图

基于时间自动机的形式化模型，使用UPPAAL可以很快建立出时间自动机的图形化模型。使用图4所示工具栏中的“创建位置”功能，可以创建时间自动机位置集合N中的所有位置。双击图中的具体位置节点，可以编辑此位置的名称、不变性约束与节点类型(包括初始状态，紧迫状态和原子状态)信息，如图5左侧所示。

图5 编辑时间自动机的位置和边

使用图4所示工具栏中的“创建边”按钮可以创建时间自动机边的集合E中的所有状态转换边。双击图中具体的边，可以编辑此状态转换边的守卫约束、发送接收消息和需要重新赋值或者归零的时钟变量与属性变量，如图5右侧所示。

使用UPPAAL的模拟器界面进行时间自动机模型的仿真。UPPAAL的模拟器界面如图6所示。

图6 UPPAAL模拟器视图

图6中间所示的组装视图展示了组成时间自动机网络的所有时间自动机组件，包含了第3节中介绍的空气模型和传感器模型。

图6下侧的消息传递视图展示了在执行时间自动机位置改变的格局变换时，伴随发生的时间自动机之间的信息传递情况。

图6右侧的“变量”窗口打印出了在当前的时钟属性解释之下，时间自动机网络所有全局和私有时钟变量和属性变量的取值。

图6左侧的“使能迁移”视图列出了在此时钟解释之下，时间自动机网络中能够执行的所有的位置改变格局变换。左下的“模拟Trace”轨迹记录视图记录了模拟仿真过程经历的所有时间自动机位置改变格局变换，并支持对这些格局变换进行前进、后退、重放和保存等功能。

使用UPPAAL的验证器界面进行时间自动机网络模型性质的验证。验证器界面如图7所示。

图7 UPPAAL验证器视图

图7中，“性质列表”展示了所有已经编辑的系统性质，右侧的按钮可以对物联网系统的性质进行添加、删除等操作。在“待验证性质”中输入或者修改系统性质。在“备注”中可以添加这个系统性质的文字说明。选中一条性质，点击“开始验证”按钮，就可以在“验证进度与结果”视图中展示所设计的时间自动机网络是否满足该性质。

5 物联网温度感知系统建模验证实践

本节以温度感知物联网系统为例，进行一个相对比较完整的物联网实时系统时间自动机建模和模型仿真验证，从而对前文论述的理论研究进行实践。

5.1 温度感知物联网系统建模

5.1.1空气物理环境建模

温度感知物联网系统中，空气物联网环境包含室外温度和室内温度2个可变的温度参数，只有在系统初始化的时候，才能确定具体的室内和室外温度。如果室内温度小于室外温度，则室内温度每隔一定的时间间隔(时间间隔可变)，以一定的增量(增量可变)升高，但最高不超过室外温度。如果室内温度大于室外温度，则室内温度每隔一定的时间间隔，以一定的增量减小，但最低不低于室外温度。室内温度可以被温度传感器感知(在UPPAAL建模中体现为信号的发送)。

在UPPAAL中可以使用UPPAAL的模板功能来处理这些参数可变的情况，如图8上侧的参数栏所示，使用OUTSIDE_TEMPERATURE代表室外温度，INIT_TEMPERATURE代表初始的室内温度，INTERVAL代表温度变化间隔，布尔变量INC代表进行温度的增加或者降低，INCREMENT代表每次温度变化的增量。

图8 使用模板建模空气温度时间自动机模型

声明了可变参数后，在建模时就可以将可变参数视为已知的量，在时间自动机模型变量声明时直接使用，如图8下侧所示的“变量”声明中进行空气温度的初始化时，使用了INIT_TEMPERATURE，对小屋的初始温度进行赋值。

在需要建模一个具体的空气温度时间自动机模型时，只需要在“模型声明”中填入参数并引入系统，就可以很快完成不同资源组件的建模。假定在夏季室外温度50 ℃，室内初始温度为35 ℃，温度每100个时间间隔上升1 ℃；而在冬季室外温度为0 ℃，室内初始温度为15 ℃，每100个时间间隔下降1 ℃。如图9所示，分别完成了夏季和冬季空气温度物理环境的建模。

图9 使用模板创建空气温度时间自动机模型的声明

5.1.2温度传感器建模

温度感知系统使用了三个温度传感器(可以基于温度传感器模板声明接入更多的传感器)进行温度的感知。在云端实现了一个温度传感器管理服务，来管理和展示温度传感器的工作状态，并收集温度传感器感知的温度数据。

温度传感器每隔一定的时间间隔进行一次温度感知，并将感知到的温度发送给云端温度传感器管理服务。如果在规定的时间间隔内温度传感器没有完成温度感知，则认为温度传感器发生了故障。按照温度传感器建模要点，我们可以很快使用UPPAAL建立温度传感器的时间自动机模板，如图10所示。

图10 温度传感器时间自动机模板

可以观察到，相比于图3讨论的温度传感器模型，图10中温度传感器时间自动机模型多出了一个sent状态，这是由于在UPPAAL中，不能在一个有向边上同时处理2个消息的发送或者接收，为了建模温度传感器从空气物理环境中感知温度并将感知到的结果发送给云端服务的行为，引入了一个虚拟的状态。我们给这个虚拟的sent状态一个原子状态的属性，在sent节点没有任何时间流逝的格局变换，在温度传感器通过GetAirTemperature感知外部温度，并通过SentAirTemperature发送温度数据到云端服务的过程中，不会被时间自动机网络中其他任何的格局变换所打断，从而达到了将sent状态和run状态合并为一个状态建模的目的。

5.1.3云端管理服务建模

云端温度传感器管理服务在运行时启动时钟计数器开始计时，接收所有温度传感器实体发送的温度并归零计时时钟，如果10个时间单位都没有接收到任何温度传感器发送的温度信息，则认为所有的温度传感器都故障了，服务指示出温度传感器故障状态。云端温度传感器管理服务的时间自动机模型如图11所示。

图11 温度传感器管理服务时间自动机模型

值得注意的是，在云端温度传感器管理服务模型中，将c>10作为进入故障状态的守卫约束，而不是run状态的不变性约束。这是因为温度传感器管理服务建模与温度传感器是不同的，温度传感器陷入故障状态的行为与其时钟计数器无关。因此在图3和图10对于温度传感器的建模中，进入故障状态是无条件的。但是云端温度传感器管理服务则不同，故考虑温度传感器管理服务的实现方式：定义一个时钟从服务开始工作的时候计时，如果接收到温度传感器发送的消息，就把时钟归零；实现一个守卫进程来实时监测时钟计数器的取值，当发现其计数值大于10的时候，就使得服务展示温度传感器故障状态。重点在于，当服务进入故障状态的一瞬间，必然有时钟计数器计数结果大于10。因此c>10是云端温度传感器服务进入故障状态的必要条件，所以将c>10作为守卫约束更加准确。

5.1.4温度感知系统模型组装

按照夏季参数，将图8所示的空气温度物理环境模板初始化为空气温度时间自动机模型；按照每10个时间单位将图10所示温度传感器物理实体模板进行温度感知创建时间自动机模型；最后将图11所示的温度感知云端服务时间自动机模型组装起来形成物联网系统时间自动机网络，如图12所示。在这个物联网系统中，接入3个温度传感器，在对大规模性的实际系统建模时可以接入更多，只要为温度传感器多声明一个实例并接入物联网系统时间自动机网络即可。

图12 温度感知服务物联网系统时间自动机模型组装

5.2 温度感知物联网系统模型验证

5.2.1温度感知系统模型仿真

通过UPPAAL的仿真工具验证了物联网系统时间自动机模型具有正确的感知温度的功能。如图13所示，当温度传感器进行温度感知的时候，空气物理环境的温度SummarAir.temperature就被赋值给系统全局变量X。此时在“使能迁移”的视图[17]中，只能继续进行温度发送这一唯一的格局变换。当执行完温度发送的格局变换时，空气物理环境的温度就被赋值到云端温度感知服务的Manager.temp中(被物联网系统采集感知)，如图14所示，由此证明了此物联网系统能够有效感知温度。

图13 温度传感器感知空气温度

图14 温度传感器发送温度到云服务

5.2.2温度感知系统模型验证

通过UPPAAL的验证器来验证所设计的温度感知物联网系统具有动态性和容错性。本文期望所有传感器都可以进入故障状态，用UPPAAL的验证语言表述为：

E〈〉Sensor1.fault

这里只给出了传感器1的验证表达式，传感器2和传感器3完全类似。

为了体现系统具有不会死锁的系统活性，将期望只要任意一个传感器还在运行，温度感知系统就不会陷入死锁，使用UPPAAL的验证语言表述为：

A[](Sensor1.run or Sensor2.run or Sensor3.run)

imply not deadlock

为了体现系统具有容错性，将期望只要传感器不全部发生故障，温度管理服务就处于正常状态，UPPAAL验证语言表述为：

A[]not (Sensor1.fault and Sensor2.fault and

Sensor3.fault) imply Manager.run

将上述3条验证语言表述输入验证器，使用3.5节中介绍的方法进行模型检测，检测的结果，如图15所示。证明了此温度感知的物联网系统具有动态性和容错性，且具有不会死锁的系统活性。

图15 温度感知虚拟实体服务模型检测

6 结 语

时间自动机建模与模型检测是验证物联网系统设计正确性的重要方法。本文从时间自动机的理论、时间自动机建模工具的层面上，结合物联网温度感知系统的建模实践，对使用时间自动机进行物联网系统的建模方法、模型仿真和模型检测方法以及建模时容易陷入的误区进行了比较完整和详细的论述，为使用时间自动机进行物联网系统建模的建模者和研究者提供了一些比较完善的经验和一个很好的建模参考。

未来可研究如何将时间自动机理论和建模方法应用到物联网系统和物理信息融合系统的建模中，从而丰富时间自动机的建模应用面，积累更多的时间自动机建模经验。

还可研究如何更好地利用物联网系统时间自动机模型，比如怎样将时间自动机中描绘的时钟属性约束和格局变换转换为软件工程中可实现编码的方法，而后在构件运行平台和代码生成工具的支持下实现物联网系统资源的自动组装和系统服务代码的直接生成，从而缩小物联网系统时间自动机模型到系统实现之间的距离，提高物联网系统建设的效率，降低物联网系统的实现成本。