信息物理融合系统的随机行为建模与验证方法研究

Modelling and model checking of CPS stochastic behaviors are challenging issues of CPS basic research, which has become increasingly prominent with widespread use of complex, large-scale CPS and active demand for enhancing the reliability and predictability. The existing CPS research is lack of a unified theory, approach and tools, which is facing the challenging to develop large-scale, safety-critical CPSs. To solve this problem, this proposal combines model-driven approach and statistical model checking(SMC) to conduct innovative research on model-driven modelling and SMC for CPS, which is under the key scientific problem "Modelling and model checking of CPS stochastic behaviors":1)Presenting the extended modelling language based on SysML/ModelicaML to model the closely related stochastic behaviors and energy consumption; 2)A SMC-based qualitative and quantitative verification approach is proposed to analyze stochastic behaviors and reliability of CPS from both of the macro and micro perspectives; 3)Developing a prototype tool and conducting empirical case studies. Our aim is to explore a model-driven approach for modelling CPSs and an innovation method based on SMC to evaluate the reliability and energy consumption. Our proposal presents a novel research solution for modelling and model checking of CPS stochastic behaviors.

建模、验证信息物理融合系统CPS的随机行为是CPS基础研究面临的挑战性问题。复杂、大规模CPS系统的广泛应用及对提高系统可靠性、可预测性的迫切需求使得该问题日益突出。针对建模、验证CPS的随机行为缺乏系统的理论、方法及工具，难以大规模开发高可信CPS系统的现状，本项目围绕"CPS随机行为建模与验证方法"这一关键科学问题，开展模型驱动式CPS随机行为建模与统计模型检测SMC的创新研究：1）针对CPS行为的随机性，扩展建模语言SysML/ModelicaML，研究模型驱动式CPS随机行为建模方法；2）研究基于SMC的定性与定量融合验证方法，结合宏观和微观分析系统的可靠性并定量评估随机行为对可靠性的影响；3）开发原型工具并研究案例实证。研究旨在探索模型驱动式CPS随机行为建模方法及基于SMC分析系统随机行为的验证方法，以期为建模、验证CPS随机行为提供一种新的研究思路，具有重要理论及实践意义。

建模、验证信息物理融合系统CPS的随机行为是CPS基础研究面临的挑战性问题。复杂、大规模CPS系统的广泛应用及对提高系统可靠性、可预测性的迫切需求使得该问题成为CPS领域关注的热点问题。针对建模、验证CPS的随机行为缺乏系统的理论、方法及工具，难以大规模开发高可信CPS系统的现状，围绕“CPS随机行为建模与验证方法”这一关键科学问题，开展模型驱动式CPS随机行为建模与统计模型检测SMC的研究。主要研究内容包括：.1）针对CPS异构、混成、随机、实时等特性，研究扩展标准建模语言MARTE/SysML，建模CPS结构及随机行为。提出了面向CPS的协同建模方法，支持从需求分析、领域模型到可执行模型的构建，为建模者提供一个集成的、多视角的建模平台；2）研究基于统计模型检测的定性与定量融合验证方法。提出基于抽象和学习的统计模型检测，将抽象技术和机器学习技术应用于统计模型检测的系统轨迹模拟生成及抽象模型构建，有效降低系统模型的复杂度、减少验证算法分析的轨迹的数量，大大提高了统计模型检测的效率。此外，基于分布式技术，设计、实现了分布式统计模型检测器，为CPS的验证分析提供多样、灵活的验证算法；3）设计、实现了CPS协同仿真语言及协同仿真环境。针对CPS异构性特征，提出基于FMI标准，设计、实现协同仿真语言，并基于GEMOC实现了该协同仿真环境。4）开发原型工具并研究案例实证。设计、实现了面向CPS的建模与验证集成工具平台，主要功能包括基于MARTE/SysML的建模、基于AL-SMC的统计模型验证器、基于FMI的协同仿真器。所取得的研究成果可推广应用到CPS的典型应用领域：能耗感知的智能建筑、轨道交通控制系统、机器人路径规划。总之，所提出建模CPS系统随机行为的方法及基于SMC的统计模型检测的研究成果具有创新性，为本领域的其他研究人员提供了一种新的研究思路，具有重要理论及实践意义。