计算机应用

作者：武鹏, 吴尽昭

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

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

基金：国家自然科学基金资助项目（61772006）。

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

来源：2021年第8期

《计算机应用》期刊编辑部

查看计算机应用杂志2021年第8期