基于CPS的实时系统的面向方面的形式化验证方法

摘要

Cyber-physical网络环境下的实时系统是一个综合计算、网络和物理环境的多维复杂系统,通过3C(Computation、Conmunication、Control)技术的有机融合与深度协作,实现大型工程系统的实时感知、动态控制和信息服务。Cyber-physical网络环境下的实时系统实现计算、通信与物理系统的一体化设计,可使系统更加可靠、高效、实时协同,具有重要而广泛的应用前景。近年来,Cyber—physical网络环境下的实时系统不仅已成为国内外学术界和科技界研究开发的重要方向,预计也将成为企业界优先发展的产业领域。开展Cyber-physical网络环境下的实时系统研究与应用对于加快我国培育推进工业化与信息化融合具有重要意义。
　　 本文试图建立一种面向方面的实时系统形式化验证方法,这种方法对形式化验证方法的进行了面向方面的扩展。以分布式实时软件非功能特性的面向方面的形式化模型为基础,研究Cyber-physical网络环境下的实时系统非功能特性的面向方面验证理论、方法和关键技术,利用面向方面的技术解决由Cyber-physical网络环境下的实时系统非功能特性的带来的验证问题的复杂性控制,使得Cyber-physical网络环境下的实时系统非功能特性的能在自动化程度和系统规模上适应系统的需要。Cyber-physical网络环境下的实时系统非功能特性的的多种特性使得验证的复杂性呈指数爆炸,在形式验证中可以采用面向方面的技术进行有效的抽象和分解。
　　 由于CPS和待检验的性质可分别表示成一个逻辑公式,要想检验系统是否满足该性质,只需在逻辑系统中检验此二公式是否有蕴含关系；同样,要想检验系统和一个方面模块之间是否具有蕴含关系,只需验证方面模块和系统相应的逻辑公式是否具有蕴含关系。在第三章中我们将看到,一种面向方面的VDM++方法对于建立系统模型非常有效。在第四章中我们将看到一个应用的例子——空中交通管制的语音通信系统,并应用基于面向方面的VDM++对系统进行验证。
　　 本文的工作重点就是要提出Cyber-physical网络环境下实时系统的形式化验证方法,提出面向方面的非功能需求框架,主要研究将面向方面的形式化验证方法技术用于Cyber-physical网络环境下实时系统非功能性需求中的研究,主要采用面向方面的VDM++方法。并在空中交通管制的语音通信系统中得到了应用。