信息物理融合系统建模与验证关键技术研究

In the times of information and network, the ability of physical equipment in computating, communicating and controling (we regard them as 3C) is becoming stronger and stronger, a new system which we call it CPS (cyber-physical system) appears in front of us, and it integrates 3C techniques and is becoming a research hot point problem in both academics and industrials, and right now its research and development are in fact not only widely concerned by many academic organizations and industries, but also supported strongly by many govenments. With the wide applications in different domains, it is becoming more and more important to ensure that some key properties, such as safety, liveness, temporal property, reliability and trustworthy,sould be satisfied by CPS; and some key algorithms and protocols used in CPS should be efficient and correct. In this project, starting from observing and analyzing the research trace of traditional embeded system and hybrid system, using for reference the successful experience of the modeling, verification, and validation of embeded system and hybrid system, we plan to use an extended UML modeling language (we regard it as UML4CPS, which denotes UML for CPS) and DDL(differential dynamic logic) to model CPS and describe properties, algorithms and protocols, and further verify these key properties, algorithms and protocols of CPS by using PSC (property sequence chart), DDL proof rules and other means. The gaol of this project is to build a complete theory or methodology to model and verify CPS. Some intelligent transport systems are used as example CPS for showing how to performing formal verification of key properties, algorithms and protocols, also for empirical analysis and evaluation.

在信息化和网络化的浪潮中，物理设备的计算、通信和控制能力日益增强，将三者融为一体的信息物理融合系统（CPS）的研究和开发近年来不仅受到学术机构和企业界的广泛关注，还受到很多国家政府的大力支持。而随着CPS在各行各业的推广应用，CPS本身一些关键属性（如安全性、时态属性、可靠性和可信性等）以及关键算法和协议是否满足需求就显得特别重要。本项目从考察传统的混成系统研究过程出发，借鉴混成建模与属性验证的成功经验，拟用一种扩展的UML建模语言、属性序列图（PSC）和微分动态逻辑（DDL）分别对CPS进行软件规约、建模与形式验证，通过引入PSC和扩展的DDL证明规则，力争对CPS系统的关键属性、算法和协议进行系统地描述和验证。本项目旨在建立一套完整的针对CPS的软件规约、建模与验证理论和方法。研究过程中还结合智能交通系统等实际CPS，对其关键属性、算法和协议进行深入的形式验证、实证分析和评估。

（1）为解决微分时态动态逻辑（dTL）表达能力弱以及微分代数动态逻辑(DAL)缺少时序表达能力的问题，提出了一种结合dTL和DAL的微分代数动态时态逻辑（DATL）。采用微分代数程序（DAP）作为操作模型，使DAL具有dTL的时序处理能力。定义了DATL操作模型的DAP和DATL语法，给出了DAP的迹语义和DATL语义，在继承dTL和DAL规则的基础上新增了6个规则。通过对飞机避撞系统安全性的规约和验证，检验了DATL的有效性。（2）定义了微分代数程序的迹语义，使得利用微分代数程序建立的模型对带有时序特征的属性规约和验证时发挥作用；定义了DATL公式的语法和语义，利用DATL对带有时序特征的CPS属性进行规约； 在继承微分代数动态逻辑(DAL)和微分时序动态逻辑增(dTL)规则的基础上，增加了六条新规则，并对这些规则给予了合理性证明；验证了三维飞机避撞系统中带有时序特征的安全性属性。