Formal Verification of a Topological Spatial Relations Model for Geographic Information Systems in Coq

被引：7

作者：

Yan, Sheng ^{[1
]}

Yu, Wensheng ^{[1
]}

机构：

[1] Beijing Univ Posts & Telecommun, Sch Elect Engn, Beijing Key Lab Space Ground Interconnect & Conver, Beijing 100876, Peoples R China

来源：

MATHEMATICS | 2023年 / 11卷 / 05期

基金：

中国国家自然科学基金;

关键词：

formal verification; set theory; general topology; topological spatial relations; geographic information systems; Coq; SETS;

D O I：

10.3390/math11051079

中图分类号：

O1 [数学];

学科分类号：

0701 ; 070101 ;

摘要：

Geographic information systems have undergone rapid growth for decades. Topology has provided valuable modeling tools in the development of this field. Formal verification ofthe model of topological spatial relations can provide a reliable guarantee for the correctness of geographic information systems. We present a proof of the topological spatial relations model that has been formally verified in the Coq proof assistant. After an introduction to the formalization of the axiomatic set theory of Morse-Kelley, the formal description of the elementary concepts and properties of general topology is developed. The topological spatial relations between two sets are described by using the concept of the intersection value. Finally, we formally proved the topological spatial relations between two sets which are restricted to the regularly closed and the planar spatial regions. All the proof details are strictly completed in Coq, which shows that the correctness of the theoretical model for geographic information systems can be checked by a computer. This paper provides a novel method to verify the correctness of the topological spatial relations model. This work can also contribute to the creation and validation of various geological models and software.

引用

页数：18