| 信息物理融合系统可信软件形式化建模与分析 |
| |
| 引用本文： | 于振华,蔡远利,付晓,谢文军,徐海平.信息物理融合系统可信软件形式化建模与分析[J].系统工程理论与实践,2014,34(7):1857-1867. |
| |
| 作者姓名： | 于振华 蔡远利 付晓 谢文军 徐海平 |
| |
| 作者单位： | 1. 空军工程大学 信息与导航学院, 西安 710077;2. 飞行器控制一体化技术重点实验室, 西安 710065;3. 西安交通大学 电子与信息工程学院, 西安 710049;4. Department of Computer and Information Science, University of Massachusetts Dartmouth, North Dartmouth 02747 |
| |
| 基金项目： | 国家自然科学基金(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可信软件进行建模和分析.
|
| 关 键 词： | 信息物理融合系统 可信软件 Petri网 π演算 建模 演化 |
| 收稿时间： | 2012-09-07 |
Formal modeling and analyzing high-confidence software of cyber-physical systems |
| |
| YU Zhen-hua,CAI Yuan-li,FU Xiao,XIE Wen-jun,XU Hai-ping.Formal modeling and analyzing high-confidence software of cyber-physical systems[J].Systems Engineering —Theory & Practice,2014,34(7):1857-1867. |
| |
| Authors: | YU Zhen-hua CAI Yuan-li FU Xiao XIE Wen-jun XU Hai-ping |
| |
| Institution: | 1. School of Information and Navigation, Air Force Engineering University, Xi'an 710077, China;2. Science and Technology on Aircraft Control Laboratory, Xi'an 710065, China;3. School of Electronic and Information Engineering, Xi'an Jiaotong University, Xi'an 710049, China;4. Department of Computer and Information Science, University of Massachusetts Dartmouth, North Dartmouth 02747, USA |
| |
| Abstract: | 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 proved directly on the structure of Petri nets. π-calculus is used to describe CPS software evolution, including agent joining, exiting, updating, and architecture reconfiguration. The evolving strategy of agents and the consistency of CPS software can also be analyzed using π-calculus. HCSFM will improve the dependability of CPS software. HCSFM is applied to unmanned ground vehicles CPS, which shows that it can effectively describe and analyze the high-confidence software of cyber-physical systems. |
| |
| Keywords: | cyber-physical systems high-confidence software Petri nets π-calculus model evolve |
| 本文献已被 CNKI 等数据库收录！ |
| 点击此处可从《系统工程理论与实践》浏览原始摘要信息 |
| 点击此处可从《系统工程理论与实践》下载免费的PDF全文 |
|
