信息物理融合系统可信软件形式化建模与分析  

Formal modeling and analyzing high-confidence software of cyber-physical systems

作　　者：于振华[1,2] 蔡远利[3] 付晓[1,2] 谢文军[1] 徐海平 

机构地区：[1]空军工程大学信息与导航学院 [2]飞行器控制一体化技术重点实验室 [3]西安交通大学电子与信息工程学院 [4]Department of Computer and Information Science,University of Massachusetts Dartmouth,North Dartmouth 02747

出　　处：《系统工程理论与实践》2014年第7期1857-1867,共11页Systems Engineering-Theory & Practice

基　　金：国家自然科学基金(61202128);航空科学基金(20100796004;20125896020);陕西省自然科学基金(2011JQ8011)

摘　　要：从多Agent系统的角度,以Petri网和π演算为语义基础,建立了一种信息物理融合系统(cyber-physical systems,CPS)可信软件形式化模型(high-confidence software formal model,HCSFM).HCSFM以Petri网形象地描述CPS可信软件静态结构模型及动态行为,用Petri网分析方法和支持工具对模型进行分析和验证;利用π演算刻画CPS可信软件中Agent的加入、退出、更新和体系结构重配置等动态演化机制,并研究Agent的演化策略及演化后CPS的一致性,确保动态演化后CPS软件能正常交互,从而为CPS软件设计提供可信保障.通过HCSFM在无人驾驶车辆编队CPS中的应用,表明HCSFM可以有效地对CPS可信软件进行建模和分析.From the perspective of multi-agent systems, a high-confidence software formal model （HCSFM）of cyber-physical systems （CPS） based on two complementary formalisms, namely Petri nets and π-calculus,is proposed. Petri nets are employed to visualize the architecture and model the behaviors of CPS software,and the structural analysis techniques allow the qualitative analysis of properties that may be proveddirectly on the structure of Petri nets. π-ealculus is used to describe CPS software evolution, includingagent joining, exiting, updating, and architecture reconfiguration. The evolving strategy of agents and theconsistency of CPS software can also be analyzed using π-calculus. HCSFM will improve the dependabilityof CPS software. HCSFM is applied to unmanned ground vehicles CPS, which shows that it can effectivelydescribe and analyze the high-confidence software of cyber-physical systems.

关 键 词：信息物理融合系统 可信软件 PETRI网 Π演算 建模 演化 

分 类 号：TP301[自动化与计算机技术—计算机系统结构]