声明
严正声明：本站非期刊官网，非中介代理。
本站仅提供学术规范服务：快速预审、润色编辑服务、中英文查重、降重、去重服务、推荐合适的期刊投稿等学术规范服务。 如需提供学术规范服务请联系在线编辑。
国内刊号：43-1258/TP
国际刊号：1007-130X
发布日期:
作者：刘永梅, 王国辉, 关永, 张景芝, 施智平, 董璐
单位：（1.首都师范大学信息工程学院，北京 100048；2.电子系统可靠性与数理交叉学科国际科技合作基地，北京 100048）
关键词：形式化验证,定理证明,格林定理,HOL Light,
基金：国家重点研发计划（2019YFB1309900）;国家自然科学基金（62002246,62272322,62272323）;科技创新服务能力建设-基本科研业务费（科研费）项目（00621530290000）
格林定理广泛应用于物理学、流体力学和化学等领域。通常使用传统的计算机仿真和数值计算方法构建基于格林定理的系统模型。然而，由于工具软件可能存在的系统缺陷导致模型出现偏差，从而使任务失败。为解决上述问题,采用基于高阶逻辑的形式化方法，在定理证明器HOL Light中实现了格林定理相关内容的高阶逻辑建模与验证。首先，对梯度、散度等基本概念和性质进行了形式化描述；其次，对格林定理及其性质进行了形式化建模与验证；最后，基于格林定理的形式化模型完成了地下水控制模型的高阶逻辑推导，进而确保系统模型的安全性。
来源：2023年第7期
《计算机工程与科学》期刊编辑部
严正声明：本站非期刊官网，非中介代理。
本站仅提供学术规范服务：快速预审、润色编辑服务、中英文查重、降重、去重服务、推荐合适的期刊投稿等学术规范服务。 如需提供学术规范服务请联系在线编辑。