论文部分内容阅读
信息-物理融合系统（Cyber-Physical System, CPS）是一种包含了嵌入式、控制、通信以及海量数据处理等技术的复杂的网络化嵌入式系统，它和物联网被认为是信息产业未来的发展方向。CPS被广泛应用在安全攸关领域，这些领域对系统可靠性具有极高的要求，因此如何保障CPS的可靠性成为一个研究热点。形式化方法是提高系统可靠性的一种有效方法，主要包括形式化建模与形式化验证两方面。由于CPS是复杂的系统，对其整体建模与验证会非常困难，针对这一问题，本文采用组合建模与验证的思路，首先将CPS分解为原子构件，再将其提供的服务建立为原子构件服务模型，然后验证原子构件服务模型的相关性质，最后建立组合服务模型并对其性质进行验证。根据上述思路，本文主要工作包括以下三个方面：（1）分析CPS的相关性质，基于混成自动机建立CPS原子构件服务模型，并分析其相关性质；（2）在CPS原子构件服务模型的基础之上，建立其组合服务模型；（3）对组合服务模型的同步/异步通信以及死锁检测进行验证，其中通信和死锁是影响系统可靠性的重要因素。最后，通过一个实例说明该模型的有效性。