半代数模型检测方法的误差分析与控制

Computer programming for automated control systems normally involves semi-algebraic systems, which consist of algebraic equalities and inequalities. Semi-algebraic model checking is a significant formal approach to verifying the correctness of control system program designs. The approach of semi-algebraic model checking admits numerical calculation of semi-algebraic systems, and in this methodology not only is the state explosion problem highly relieved, but also the practical computational requirements in control engineering are fitted perfectly. However, numerical calculation allows errors, which are a key and decisive factor for the dependability of semi-algebraic model checking. If the errors occurred are managed improperly, then a false verification result may be reached. Therefore, the errors have to be analyzed properly, and furthermore are controlled in a right manner. In this project, a theory of error analysis and control is established for semi-algebraic model checking, and its applications in automated control system programming are investigated, including: (1) the concept and the computation of well-behaved errors, (2) the decidabilities of the dependabilities of semi-algebraic model checking under well-behaved errors, in particular, (2.1) the basic dependability, (2.2) the equivalence dependability, (2.3) the abstraction dependability, and (2.4) the mixed dependability, that is, deciding respectively whether semi-algebraic model checking as well as its model equivalence, abstraction and equivalence and abstraction combined replacements preserve the correct verification result again under well-behaved errors, and (3) a prototype software tool is developed, and applied to the verification of the program designs of railway traffic control systems.

计算机自动控制系统程序一般包含由代数等式和不等式构成的半代数系统，半代数模型检测是控制系统程序设计正确性验证的一种重要形式化方法。半代数模型检测方法允许使用半代数系统的数值计算，不但可以有效缓解状态爆炸，而且契合控制工程现实的计算需要。但数值计算带有误差，误差对于半代数模型检测的可信性是个决定性的关键因素，处理不当，会导致错误的验证结果。因此必须对其进行正确的分析，进而做到合理的控制。本项目构建半代数模型检测方法的误差分析与控制理论，并在控制系统程序设计中加以应用。具体包括：(1)良性误差的定义与计算；(2)良性误差下半代数模型检测的可信性判定：(2.1)基本可信性、(2.2)等价可信性、(2.3)抽象可信性、(2.4)混合可信性，即分别判定良性误差下半代数模型检测及其模型等价、抽象以及等价和抽象混合替换是否依然保持正确的验证结果；(3)开发原型平台工具并应用于轨道交通控制系统程序设计。

面对现代控制系统规模和复杂程度的剧增等问题，如何构建确保系统设计正确性的验证方法是一个严峻挑战。状态迁移和数据交换是控制系统程序设计的关键，形式化模型检测是控制系统程序设计验证的有效手段。本课题采用半代数变迁系统刻画模型，并将数值计算引入到半代数变迁系统的分析与计算，不但可以有效缓解状态爆炸，而且契合控制工程现实的计算要求。但是数值计算带有误差，对误差进行有效控制以保证半代数模型检测的可信性是课题解决的关键问题。本课题通过形式化方法和数值计算的有机融合，构建出控制系统程序设计验证半代数模型检测方法的误差分析和控制理论，并在控制系统程序的设计中加以应用。主要的研究内容包括：第一是误差计算，研究代数函数的误差合成与分配及程序模型及性质断言的良性误差；第二是误差保持模型检测及其模型等价和抽象替换可信性，研究良性误差下半代数模型检测方法的可信性，包括基本可信性、等价可信性、抽象可信性及混合可信性四个方面；第三是工程应用，研究所构建的理论方法在轨道交通列车等控制程序设计与分析中的应用。