作　　者： ;

机构地区： 嘉应学院计算机学院

出　　处： 《计算机科学》 2014年第S1期64-66,86,共4页

摘　　要： 由于信息物理融合系统(CPS)的硬件集成度和软件参与度不断提高,大量软件与硬件间异构连通并相互控制,使得CPS的分析设计、建模与验证也愈加困难,由此引起模型的状态空间膨胀问题。提出利用带标记混合Petri网方法对CPS进行建模和验证研究,在CPS中采用模型检测和定理证明相结合的形式化方法,对试图解决系统验证时状态空间膨胀问题供理论依据。提出一种自动抽取及其简化模型的方法,在容错温度传感器系统中的初步实验结果表明该方法是可行的,通过一个实例原型的应用说明了该方法的有效性。 Because the cyber-physical system(CPS)hardware integration and software involvement in degree rise ceaselessly,many software and hardware have heterogeneous connectivity and mutual control.The analysis design,modeling of CPS have become more and more difficult.In this paper,a safety verification method based on 1abeled hybrid Petri net and differential-algebraic dynamic logic was proposed.The method firstly transforms LHPN model to differential-algebraic program,then realizas the specification of system safety using differential-algebraic program,and finally the cyber physical systems safety is verified according to differential-algebraic program reasoning rules.It is effectiveness for the method through an instance of the prototype application.

关 键 词： 带标记混合 网 信息物理融合系统 建模 验证

领　　域： [自动化与计算机技术] [自动化与计算机技术] [自动化与计算机技术] [自动化与计算机技术]