An approach to formal specification and verification of mapcentered applications

Users in the domain of map-centered applications who want to specify a new application rely only on informal languages such as English. There is also no standardized terminology, resulting in ambiguous specifications. This work proposes an approach to specify and verify map-centered applications. This domain has been studied under different perspectives but there is a lack of research from the software engineering viewpoint. We characterize the domain by presenting a classification of different space models that appear in the Geographical Information Systems (GIS) literature, as well as of some of the problems addressed by map-centered applications. The proposed solution includes a language with semantics based in a formalization of each space model. This helps in verifying properties over a specification written using the formal language.