1、本研究的背景与意义
互联网加物联网形成“智慧地球”，是当前世界性的热门课题。抓住物联网发展的这一机遇，将不仅为中国信息产业，也为“中国制造”赢得未来巨大而广阔的发展空间。可信计算已成为当前的一个热点研究领域。物联网执行的可信性问题，是物联网背后的重要科学问题之一。物联网是嵌入式系统网络化的产物。本研究针对构成物联网基础的嵌入式系统，研究其可信性问题，即分析系统在一定时间约束条件下按设计的要求正确运行的可信度（概率）。本研究推动了对物联网执行可信性的认识，可提供科学、有效的方法来分析和完善物联网执行的可信性。研究成果在嵌入式系统领域本身也具有广泛的使用价值。
2、本研究取得的重要科技成果
本研究围绕物联网中嵌入式系统的可信性验证而展开，并取得了一系列成果。以时间扩展的活性顺序图这一场景规约的形式进行嵌入式系统性质的描述，以概率时间自动机网络或概率时间扩展的活性顺序图网络建模嵌入式系统，针对系统在一定时间约束条件下满足性质的可信度（概率），开展了模型检测算法、工具及其应用的研究，取得相关成果；对于状态数目较大的嵌入式系统，针对基于假设-保证推理的组合验证方式，研究了有关的模型检测问题，取得相关成果；对于不符合性质要求的嵌入式系统，针对其可信性方案的调整进行了研究，取得相关成果。具体内容如下：
（1）基于场景规约的嵌入式系统可信验证
给出合理的建模方法：对活性顺序图(Live Sequence Chart, LSC)进行时间扩展(称这种扩展后的LSC为TLSC)，以时间扩展的LSC来描述物联网环境中嵌入式系统的性质；对LSC进行时间和概率的扩展(称这种扩展后的LSC为PTLSC)，对一个嵌入式系统的每一个重要的子系统或组件，采用一个概率时间自动机或PTLSC来描述，从而用一个概率时间自动机网络或PTLSC网络来对构成物联网的一个嵌入式系统进行建模。
研究了以TLSC描述系统性质、分别采用概率时间自动机网络和PTLSC网络建模系统时，就系统在一定时间约束条件下满足性质的可信度（概率）问题，设计和验证了相关的模型检测算法和工具，并申请了发明专利“一种基于扩展活性顺序图模型检测的物联网可信性评价方法”。
（2）物联网中复杂嵌入式系统的基于假设-保证推理的组合验证
在采用时间扩展的LSC描述系统性质时，对于物联网环境中具有大数目状态的复杂嵌入式系统，研究了以概率时间自动机网络建模时，以基于假设-保证推理的方法进行组合验证的有关问题。设计和验证了在此背景下假设-保证推理的规则、假设的产生方法等。
（3）嵌入式系统的可信性方案调整研究
当上述针对概率时间自动机网络的模型检测（即验证）出现反例时，对于出现反例的概率时间自动机，研究了其模型修复的有关问题，设计和验证了有关的算法。
通过上述研究工作，发表的论文如下：
（1）张君华等，基于抽取-精化的概率系统假设-保证验证，计算机工程与科学，2013年3月，35(3): 128-133，中文核心期刊；
（2）Zhang Junhua, Model Checking Probabilistic Timed Systems Against Timed Automata Specification，Lecture Notes in Electrical Engineering，2013.12，volume 279: 1273-1278，EI收录；
（3）Zhang Junhua等, A Formal Analysis Framework for Internet of Things，2013 2nd International Symposium on Instrumentation and Measurement, Sensor Network and Automation (IMSNA)，2013.12, Toronto，Canada， Part 1: 114-116，EI收录；
（4）Zhang Junhua, Model repair probabilistic timed systems，Journal of Convergence Information Technology，2013年1月，8(2): 537-544，2012年EI源刊。
通过上述研究工作，申请的专利如下：
（1）张君华等，一种基于扩展活性顺序图模型检测的物联网可信性评价方法，发明专利，宁波甬致专利事务所代理，2013年12月30日上报国家专利局审核。
3、本研究取得的直接（间接）经济效益及成果推广应用前景
根据上述研究成果，申请了发明专利。该发明专利提供了一种基于扩展活性顺序图模型检测的物联网可信性评价方法，通过该方法可实现对物联网可信性的评价。
该发明很好地契合了我国大规模物联网开发与利用的需要，在基于物联网是嵌入式系统的网络化这一理念的基础上，进一步地提出了由多个紧密耦合的嵌入式设备构成一个相对独立的嵌入式系统，一个物联网由多个这样的嵌入式系统，通过网络的连接而构成，从而为利用现有的实时嵌入式系统技术来分析物联网奠定了理论基础。
该发明提出利用概率时间活性顺序图来建模物联网，利用时间活性顺序图来描述物联网的运行场景，从而使得对物联网的描述摆脱了形式化描述的局限，描述直观、可视化程度高，便于该发明的推广利用。该发明的各个主要技术环节都有开源软件的支持，具有很高的可操作性，为该发明的实际利用创造了很好的条件。该发明利用了模型检测技术，因此既可用于已建成物联网（或其一部分）的可信性评估，也适合于物联网系统设计阶段的对系统开发模型的可信性评估，使用面十分广泛。
该发明提出的基于扩展活性顺序图模型检测的物联网评价方法，经过实验论证，效果可信。解决问题速度较快，对计算空间要求不高，节约成本。该发明专利经过充分的技术论证，具备充分的理论可行性和实践可行性。
本研究还对物联网中复杂嵌入式系统的验证，给出了基于假设-保证推理的组合验证方案；对不满足可信性要求的嵌入式系统，给出了调整方案。这些研究成果进一步提高了对物联网可信性的分析水平，有利于设计出更加复杂和完善的物联网系统，具有较高的实用价值。
总之，本研究提升了业内对物联网设计与运行的理论认识水平和实际检测技术水平，对加快国内物联网产业的健康和可持续发展具有重要的促进作用。目前的物联网公司往往规模不大，只研制了物联网中的部分产品，本研究中的嵌入式系统划分方法就有很强的针对性，可信性评价和优化技术具有很好的实用性。本研究成果在嵌入式系统领域本身也具有广泛的使用价值。
