多维区域匹配算法的通用验证方法  

The General Verification Method for Multidimensional Region Matching Algorithm

作　　者：张晗庆 游珍 左正康[1] 吴嘉伟[1] 程着 ZHANG Hanqing;YOU Zhen;ZUO Zhengkang;WU Jiawei;CHENG Zhuo(School of Computer Information Engineering,Jiangxi Normal University,Nanchang Jiangxi 330022,China;State International S&T Cooperation Base of Networked Supporting Software,Jiangxi Normal University,Nanchang Jiangxi 330022,China)

机构地区：[1]江西师范大学计算机信息工程学院,江西南昌330022 [2]江西师范大学网络化支撑软件国家科技合作基地,江西南昌330022

出　　处：《江西师范大学学报(自然科学版)》2024年第6期646-651,共6页Journal of Jiangxi Normal University(Natural Science Edition)

基　　金：国家自然科学基金(62462036,62102171);江西省自然科学基金(20232BAB202010,20242BAB26017);江西省教育厅科学技术研究课题(GJJ210340,GJJ2409405)资助项目.

摘　　要：区域匹配算法通常用于多维数据空间中快速匹配特定区域或数据集,被广泛应用于数据库系统、数据分发管理系统等.目前大多数区域匹配算法的实现方法效率较低且未得到正确性验证.因此,该文提出了一种多维区域匹配算法的通用验证规约,以威胁辐射源匹配算法作为实例,使用Isabelle/HOL定理证明器对其进行函数式建模.将该文实现的通用验证规约通过区域解释应用于威胁辐射源匹配算法,通过严格的机械化验证,确保了威胁辐射源匹配算法的正确性,进而验证了该方法的有效性和可扩展性.Region matching algorithms are commonly used for rapidly matching specific regions or datasets in multidimensional data spaces,and are extensively applied in database systems and data distribution management systems.However,most existing implementations of region matching algorithms exhibit low efficiency and lack formal correctness verification.In response,the general verification framework for multidimensional region matching algorithms is proposed.Subsequently,using the threat radiation source matching algorithm as a case study,the functional mode-ling with the Isabelle/HOL theorem prover is performed.Finally,the general verification framework developed in this paper is applied to the threat radiation source matching algorithm through region interpretation.Through rigorous mechanized verification,the correctness of the threat radiation source matching algorithm is ensured,thereby demonstrating the effectiveness and scalability of the proposed method.

关 键 词：多维区域匹配算法 威胁辐射源匹配算法 函数式建模 机械化验证 

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