半代数混杂系统形式化分析与验证的例证法研究

Data communication and continuously changed states are two important characteristics that have to be taken into account and tackled in the designs of complex control systems. These two crucial aspects in some degree can be entirely and systematically represented and specified by hybrid system models. Hybrid systems, however, are normally able to be approximately modeled by semi-algebraic hybrid systems. Semi-algebraic hybrid systems are therefore often used as the system models in formal analysis and verification of control system designs. In this project, a theory of instance citing approaches is constructed towards formal analysis and verification of semi-algebraic hybrid systems. Concretely, discrete instances of the given semi-algebraic hybrid system models are constructed by using algebraic symbolic computation and numerical computation, and then，based on the instance models, the instance citing approaches to (1) deciding the behaviour equivalence relations on semi-algebraic hybrid systems, (2) deciding the regional abstraction relations on semi-algebraic hybrid systems, and (3) model checking semi-algebraic hybrid systems are proposed, such that deciding the behaviour equivalence, the regional abstraction relations on semi-algebraic hybrid systems, and model checking semi-algebraic hybrid systems are able to be realized by instance models. Meanwhile, (4) the preservation properties between the instance citing approaches to deciding behaviour equivalence relations, regional abstraction relations on semi-algebraic hybrid systems and to model checking semi-algebraic hybrid systems are certified, in order that behaviour equivalence as well as regional abstraction reductions are available without any impacts on the results of model checking. One other advantage of the instance citing approaches is that they guarantee the discretization methodology for the designs of complex control systems and the analysis and verification of the designs with semi-algebraic hybrid system models can be carried on in an inherent and uniform framework.

数据交换和连续的状态变化是复杂控制系统设计必须考虑和处理的两个重要特征，混杂系统模型能够全面系统地表示和刻画这两方面的重要因素，而混杂系统通常能够用半代数混杂系统近似模拟，因而控制系统设计的形式化分析与验证一般可以采用半代数混杂系统模型。本项目构建半代数混杂系统形式化分析与验证的例证法理论，具体包括：通过代数符号与数值计算相结合，构造半代数混杂系统的离散实例，在此基础上，建立半代数混杂系统的（1）行为等价关系判定，(2)区间抽象关系判定，以及（3）模型检测的例证法，使得半代数混杂系统的行为等价、区间抽象关系判定以及模型检测在离散实例模型上实施即可，同时，证明（4）行为等价、区间抽象关系、模型检测例证法相互之间的可保持性，以保证行为等价及区间抽象约简对模型检测的结果没有影响。例证法的另一个优点是，实现了控制系统的离散化设计与基于半代数混杂系统模型的系统分析和验证能够在和谐和统一的框架内进行。

复杂控制系统大量存在于现实生活当中，如何确保控制系统设计正确性一直是个挑战。形式化方法是复杂控制系统设计分析和验证的有效手段，复杂控制系统涉及到离散的状态跳转、数据交换和连续的状态变化，这些特征使得混杂系统模型非常适合用于这些系统的刻画。同时在设计中，通常用只含有多项式等式或不等式标记的半代数混杂系统近似模拟带有微分及代数方程或不等式的混杂系统模型。而形式化混杂系统模型的构建通常由一些具体的实例归纳总结得到，是从具体到一般的归纳推理过程，这为形式化方法的例证法提供了研究方向。为此，本项目通过代数符号计算与数值计算相结合，构建了一套完整的半代数混杂系统形式化分析与验证的例证法理论，并用演绎推理的方法证明例证法的可靠性，进而构造出即满足实际工程的设计需求，又满足形式化分析和验证需要的离散实例模型，解决或部分解决了以下三个问题： 1）模型表示层面，研究了半代数混杂系统的行为等价、区间抽象关系判定的例证法，以及它们的可保持性；2）验证方法层面，研究了模型检测的例证法及其等价和抽象约简优化策略；3）工程应用层面，基于所构建的例证法开发的原型平台工具系统可应用于轨道交通列车运行控制系统的设计与分析。科学意义在于所构建的理论和方法是复杂系统设计形式化分析与验证迫切需要的，系统分析与验证工作不必在混杂系统模型上进行，只需在具体的离散实例模型上进行即可。