基于线性误差断言的推理方法  

Reasoning method based on linear error assertion

作　　者：武鹏 吴尽昭[1,2,3,4] WU Peng;WU Jinzhao(School of Computer and Information Technology,Beijing Jiaotong University,Beijing 100044,China;Chengdu Institute of Computer Application,Chinese Academy of Sciences,Chengdu Sichuan 610041,China;School of Computer,Electronics and Information,Guangxi University,Nanning Guangxi 530004,China;School of Artificial Intelligence,Guangxi University for Nationalities,Nanning Guangxi 530006,China)

机构地区：[1]北京交通大学计算机与信息技术学院,北京100044 [2]中国科学院成都计算机应用研究所,成都610041 [3]广西大学计算机与电子信息学院,南宁530004 [4]广西民族大学人工智能学院,南宁530006

出　　处：《计算机应用》2021年第8期2199-2204,共6页journal of Computer Applications

基　　金：国家自然科学基金资助项目(61772006)。

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

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

分 类 号：TP311.5[自动化与计算机技术—计算机软件与理论]