基于服务的信息物理融合系统软件结构建模方法

信息物理融合系统（简称CPS）是嵌入式计算机与物理设备紧密耦合的系统，在医疗、交通、环境监控等领域的应用日益广泛。然而，CPS结构和行为特征复杂，如何高效地开发满足应用需求的CPS软件成为具有挑战性的重要研究课题。面向服务方法通过在服务之间定义良好的接口和契约联系、 组合服务构建复杂系统，成为CPS软件设计的一种可能途径。本项目从软件结构模型的角度研究CPS的结构和行为特征，旨在建立基于服务的CPS软件结构建模核心概念和关键技术。通过定义CPS软件结构形式化语言、提出需求驱动与精化相结合的CPS软件结构建模方法，实现增量式验证技术，建立基于服务的CPS软件结构形式化模型。本项目研究对于揭示CPS的本质特性、建立CPS软件设计理论、提高CPS软件可复用性和可信度具有理论意义和应用价值。

信息物理融合系统在工业和人们日常生活领域具有广泛的应用前景，然而，CPS的结构和行为特征复杂，如何高效地开发满足应用需求的CPS软件成为具有挑战性的课题。本项目“基于服务的信息物理融合系统软件结构建模方法”对CPS的系统需求、形式化软件结构模型语言、软件结构模型设计方法、性质规范及验证技术进行了系统的研究。本项目研究的基本思路是将基于Petri网的形式化方法与基于服务的结构相结合，通过在服务之间定义良好的接口和契约联系、 优化组合服务为设计复杂系统CPS软件提供理论基础和实践方法。本项目研究的主要成果包括：（1）提出了一种基于面向方面的CPS需求获取方法，能够对CPS的设备、计算与物理交互、通信过程、构件组合等要素的需求建模；（2）对经典Petri网做了若干扩充，使之具有对CPS的时间约束、能耗管理、资源管理、服务组合优化建模能力，用于CPS融合物理实体和计算成分的动态软件结构建模；（3）提出了基于时态逻辑和融合于结构的CPS性质规范描述方法，前者适合CPS系统实时性、安全性、活性性质规格说明，后者适用于需求驱动的CPS软件设计精化；（4）针对CPS系统中计算和物理过程混杂的特性，提出了一种面向方面离散连续Petri网建模方法，将横跨系统的具有共性物理过程作为横切关注点抽取出来，通过编织规则将之与核心功能模型集成为整体模型。利用方面网和核心网的输入输出和触发规则，保证模型的一致性和正确性；（5）提出了一种增量式方法验证CPS软件结构模型的性质，并综合使用模型检查和定理证明两种验证技术。本项目研究对于揭示CPS的本质特性、建立CPS软件设计理论、提高CPS软件可复用性和可信度具有理论意义和应用价值。.通过本项目研究，在国内外重要刊物上发表学术论文61篇（含录用），其中SCI源刊13篇、EI收录22篇、 ISTP收录9篇，获得上海市科学技术进步一等奖1项，授权国家发明专利1项，培养骨干教师3名，8名研究生完成博士学业、10名硕士生获得硕士学位。