基于统计模型检测的CPS软件可信性验证研究

摘要

随着嵌入式技术、计算机技术和网络技术的不断发展,以及硬件产品性能和数据处理能力的不断提升,物联网技术得到快速发展。在此背景之下,信息-物理融合系统(Cyber-Physical Systems, CPS)作为一种新型嵌入式网络系统应运而生,并且引起了各国政府、学术界和工业界的高度重视。CPS是融合了计算和物理进程的复杂嵌入式网络系统,它通过嵌入式系统和网络对物理设备进行监测和控制,并通过反馈机制相互影响。CPS通常广泛用于重要基础设施的监测与控制、国防武器系统、医疗保健和智能交通等诸多安全攸关领域。由于物理环境通常具有不确定性以及物理设备本身可能出现故障,如何保证CPS的可信性成为一项重大的挑战,而CPS的可信性与CPS软件的可信性密切相关,因此保证CPS软件可信十分重要。形式化验证技术是提高软件可信性的一种重要技术,模型检测技术是软件验证时经常采用的形式化技术。传统模型检测技术的应用受到系统状态空间大小的限制,而CPS的状态空间巨大。统计模型检测是基于仿真和统计评估技术验证大型复杂系统的一种模型检测技术,可以对无限状态系统进行验证。
　　本文针对传统模型检测技术难以验证CPS软件的问题,采用统计模型检测技术,围绕CPS软件属性验证领域所涉及的三个核心步骤:CPS软件形式化建模、CPS软件属性静态验证及CPS软件属性运行时动态验证展开研究。首先,以混成自动机为基础,通过引入通信端口得到扩展混成自动机,建立一个可以有效表达 CPS软件行为的形式化模型;其次,基于统计模型检测技术,提出一种能够对CPS软件的行为属性进行静态验证的方法;最后,对CPS模型进行改进,考虑到环境因素对CPS运行结果的影响,对CPS中的不确定性等进行建模,并研究了CPS软件属性的运行时动态验证方法。使用统计模型检测技术对CPS软件属性进行验证,可以有效避免传统模型检测技术必须面对的状态空间爆炸问题,提升了CPS的健壮性和安全性。

目录

封面

声明

中文摘要

英文摘要

目录

第一章 绪论

1.1 研究背景及意义

1.2 国内外研究现状

1.3 本文研究内容

1.4 本文组织结构

第二章 CPS概述

2.1 CPS的定义

2.2 CPS的特征

2.3 CPS的应用

2.4本章小结

第三章 统计模型检测概述

3.1模型检测技术

3.2随机模型检测

3.3统计模型检测

3.4本章小结

第四章 基于扩展混成自动机的CPS软件建模

4.1问题描述

4.2基于扩展混成自动机的CPS软件模型

4.3实例分析

4.4本章小结

第五章 基于统计模型检测的CPS软件静态验证

5.1 CPS软件静态验证框架

5.2 CPS软件的统计模型检测

5.3实例分析

5.4本章小结

第六章 基于统计模型检测的CPS软件动态验证

6.1 CPS软件动态验证框架

6.2 CPS软件动态验证

6.3实例分析

6.4本章小结

第七章 总结与展望

7.1本文工作总结

7.2未来工作展望

参考文献

攻读硕士学位期间参加的科研项目和获得的科研成果

致谢