中文摘要：

设备协同技术是物联网的核心支撑技术之一，其可信性保障是应用、实施和部署物联网的过程中需要解决的重要问题，也是促使物联网从概念走向应用的关键。本项目将围绕着可信设备协同的建模与验证方法展开研究。首先，为保证演化行为的可信性，拟在PI演算的基础上，扩展其对系统状态的全生命周期管理能力及对用户非功能属性需求刻画能力，提出一种基于带类型约束的扩展PI演算的设备协同行为模型；其次，为保证演化过程的可信性，拟对协同动态演化流程及其执行的关键特性及操作进行明确定义，给出协同演化的执行路径和精确执行语义；再次，为保证演化实施的可信性，拟对环境进行建模，将用户需求和运行环境的动态变化刻画在流程执行上下文中，协同流程的运行在环境中被观察和评估实现协同可信性分析与验证；最后，通过原型系统进行模拟仿真，以验证提出方法的有效性。

结论摘要：

从立项至今，围绕物联网可信设备协同的建模和验证这一主题，严格按照计划书的要求积极开展研究工作，认真完成科研任务，严格执行既定预算，最终取得了若干研究成果，并积极投入应用实践，获得了良好效果，完成了预期目标。现从所获研究成果，成果应用和成果意义三面加以介绍。 1.所获成果 (1)研究了设备协同系统设备建模问题，提出了基于DC-PI演算的设备协同系统设备的建模方法； (2)研究了设备协同流程形式化问题，提出了基于DC-PI演算的设备协同流程及其执行的形式化描述方法； (3)研究了设备协同流程分析与验证问题，提出了环境驱动的设备协同流程分析与验证方法； (4)研究了设备协同的验证过程，提出了集成化验证框架的概念，并开发了相应软件系统一套。 2.成果应用 (1)利用DC-PI演算，对上海世博园周边报警子系统和视频监控子系统进行了建模，给出了系统的形式化的模型定义； (2)以DC-PI演算协同流程定义为基础，对上海世博园周边报警联动系统和视频监控子系统联动为例，对其协同流程进行了建模； (3)给出了上海世博园周边报警系统和视频监控系统环境和需求的定义，分析和验证了其协同流程的业务属性； (4)利用开发的PICal2NuSMV工具，以智能交通协同控制为例，进行了形式化的分析和验证，确保了控制过程的可信性。 3.成果意义 (1)DC-PI演算的提出，解决了传统建模和分析方法中对于非功能属性表达不足的缺点，有效地简化了设备协同流程及其业务逻辑的建模和验证，保证了设备协同演化行为的可信性； (2)基于DC-PI演算的协同流程形式化语义的提出，解决了传统方法中对于协同演化过程分析缺乏精确定义的不足，提供一个统一的底层形式化语义平台，保证了设备协同演化过程的可信性； (3)基于环境的设备协同流程分析与验证方法的提出，解决了传统分析方法中忽略环境因素的问题，确保整个设备协同流程运行可靠、用户既定需求得以满足，保证了设备协同演化实施的可信性； (4)集成验证平台的构建，为系统研发人员提供了有效、自动化的系统建模和验证工具，保证了系统验证过程的可信性。 在基金委的资助下，发表学术论文十一篇，组织国际会议一场，申请专利八项，参加相关学术会议两场，开发软件系统一套，培养博士两名。