论文部分内容阅读
信息物理融合系统(Cyber Physical Systems,CPS)是一种高级嵌入式系统,它将数字计算系统与物理过程结合起来,更关注计算机与物理环境的交互和协作。自概念被提出以来,CPS一直受到学术界与工业界的高度关注。由于CPS大都是异构的混成系统,处于开放环境中,又融合了连续的物理过程和离散的计算机系统行为,因此CPS具有异构性、不确定性、连续性等特性。同时,由于CPS的应用大都与安全相关或对功耗的要求严苛,因此在保证功能的前提下,仍须满足一定的非功能属性(Non-Functional Properties,NFP),如时间、能耗等,因而CPS的非功能属性也是研究的一个方面。针对这种异构系统的建模问题一直是人们研究的重点,但是,现如今仍缺乏系统性的方法来建模CPS的特性。为了更系统地建模CPS的异构性、随机性、连续性和非功能属性等,本文提出了一种基于SysML/MARTE/pCCSL的协同建模方法,实现从不同视角建模CPS的不同特征,包括系统的结构、行为、时钟约束和NFP。首先,为了捕捉CPS的特性如异构性和连续行为,扩展了四个SysML/MARTE的元模型,包括需求图、块定义图、内部框图和状态机图。针对CPS的随机行为,基于时钟约束规范语言(Colck Constraint Specification Language,CCSL),增加了三个操作符,得到扩展的pCCSL,以建模CPS的随机行为并对模型进行精化。pCCSL作为一种时钟约束语言,可以规约各模型之间的交互和同步,显式地建模多视图模型之间的逻辑一致性。其次,为了系统地建模CPS,提出了一种基于SysML/MARTE/pCCSL的协同建模方法,旨在从不同视角建模CPS的不同特征。该方法的新颖之处在于使用逻辑时钟来驱动和协调不同模型,并以模型驱动的方式,为开发高质量的CPS系统提供了一种基于标准可视化建模语言的协同建模方法。然后,针对使用pCCSL进行精化的模型,为了探索不同方案的可行性并推动模型的精化过程,提出了从MARTE/pCCSL转换为随机混成自动机(Stochastic Hybrid Automata,SHA)的映射规则,以期使用统计模型检测(Statistical Model Checking,SMC)对模型进行验证、评估,帮助设计人员优化系统模型。为了实现扩展的SysML/MARTE元模型和pCCSL,我们开发了基于GeMoC的工具集。最后,为了证明所提出建模方法和各扩展的元模型的可行性,针对“智能建筑系统”这一具体案例进行了建模和精化,并对精化后的模型进行了验证和评估。实验证明了该协同建模方法的可行性,并且可以借助统计模型检测技术对系统进行验证分析。