Abstract: Errors are common to the system. In safety-critical systems, quantitative analysis of errors is necessary. However, the previous reasoning and verification methods rarely consider errors. The errors are usually described with the interval numbers, so that the linear assertion was spread and the concept of linear error assertion was given. Furthermore, combined with the properties of convex set, a method to solve the vertices of linear error assertion was proposed, and the correctness of this method was proved. By analyzing the related concepts and theorems, the problem to judge whether there was implication relationship between linear error assertions was converted to the problem to judge whether the vertices of the precursor assertion were contained in the zero set of the successor assertion, so as to give the easy-to-program steps of judging the implication relationship between linear error assertions. Finally, the application of this method to train acceleration was given, and the correctness of the method was tested with the large-scale random examples. Compared with the reasoning methods without error semantics, this method has advantages in the field of reasoning and verification of systems with error parameters.

Key words: formal method, theorem proving, reasoning method, implication relation, error theory

摘要： 误差在系统中是普遍存在的。在安全关键系统中，对误差的定量分析是必要的，而以往的推理验证方法较少考虑误差。误差通常用区间数来刻画，从而推广了线性断言，并给出了线性误差断言的概念。此外，结合凸集的性质，提出了求解线性误差断言顶点的具体方法，并验证了该方法的正确性。通过分析相关概念及定理，将判断线性误差断言之间的蕴含关系的问题转化为前驱断言的顶点是否被包含在后驱断言的零点集的判断问题，从而给出了判断线性误差断言的蕴含关系的具体方法步骤，且该方法易于在计算机上编程实现。最后，给出该方法在火车加速状态上的应用，并且用大量随机实例测试了该方法的正确性。与不含误差语义的推理方法相比，该方法在含误差参数的系统的推理验证领域是有优势的。

关键词: 形式化方法, 定理证明, 推理方法, 蕴含关系, 误差理论