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

Sheng Yan () and Wensheng Yu
Additional contact information
Sheng Yan: Beijing Key Laboratory of Space-Ground Interconnection and Convergence, School of Electronic Engineering, Beijing University of Posts and Telecommunications, Beijing 100876, China
Wensheng Yu: Beijing Key Laboratory of Space-Ground Interconnection and Convergence, School of Electronic Engineering, Beijing University of Posts and Telecommunications, Beijing 100876, China

Mathematics, 2023, vol. 11, issue 5, 1-18

Abstract: 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.

Keywords: formal verification; set theory; general topology; topological spatial relations; geographic information systems; Coq (search for similar items in EconPapers)
JEL-codes: C (search for similar items in EconPapers)
Date: 2023
References: View references in EconPapers View complete reference list from CitEc
Citations: View citations in EconPapers (2)

Downloads: (external link)
https://www.mdpi.com/2227-7390/11/5/1079/pdf (application/pdf)
https://www.mdpi.com/2227-7390/11/5/1079/ (text/html)

Related works:
This item may be available elsewhere in EconPapers: Search for items with the same title.

Export reference: BibTeX RIS (EndNote, ProCite, RefMan) HTML/Text

Persistent link: https://EconPapers.repec.org/RePEc:gam:jmathe:v:11:y:2023:i:5:p:1079-:d:1076013

Access Statistics for this article

Mathematics is currently edited by Ms. Emma He

More articles in Mathematics from MDPI
Bibliographic data for series maintained by MDPI Indexing Manager ().