邵小东，郭继发

(1.云南省烟草公司红河州公司，云南 弥勒 652399；2.天津师范大学 城市与环境科学学院，天津 300387)

形式化描述方法在地理信息系统中应用综述

邵小东1，郭继发2

(1.云南省烟草公司红河州公司，云南 弥勒 652399；2.天津师范大学 城市与环境科学学院，天津 300387)

总结形式化理论与地理信息系统的应用情况，阐述形式化描述方法在空间拓扑关系、距离关系与方向关系等方面的应用。文中提出形式化方法在地理信息系统问题框架描述与多系统接口描述中的应用，即通过形式化方法精确一致的规格化描述定义，促进对地理信息领域问题的更好理解，促进信息融合，提高地理信息系统开发质量。

形式化方法；形式化模型；地理信息系统；应用综述

形式化方法是基于严密的、数学上的形式机制的系统研究方法。客观地讲，有了数学的应用，就有了形式化方法。从广义角度讲，形式化方法是软件开发过程中规格、设计及实现的系统工程方法；狭义上，形式化方法是软件规格和验证的方法。因此，形式化方法又分为形式化规格和形式化验证法方法[1]。

1 形式化与地理信息系统结合应用

目前，纵观国内外所刊文献资料，形式化描述在空间信息系统方面的应用主要集中在空间拓扑关系、距离关系与方向关系等方面。空间关系描述的基本任务是以数学逻辑的方法区分不同的空间关系，给出形式化的描述。其意义在于澄清不同用户关于空间关系的语义，为空间关系判断、推理，构造空间查询语言和空间分析提供形式化工具。

1.1 线面拓扑关系描述

针对面目标间的拓扑关系描述，已建立一些形式化描述模型，如基于空间逻辑的RCC模型(Region Connection Calculus)[2]、空间代数模型[3]，以及四交模型[4]和九交模型[5]等。邓敏、刘文宝等建立一种GIS中面目标间拓扑关系形式化描述和区分的广义模型[6]。

针对线目标间拓扑关系的描述，建立的一些形式化描述模型都有一定的空间目标间拓扑关系表达能力，如九交模型能区分线与线之间的33种拓扑关系[7]。张水舰、李永树以点集拓扑学基本理论为基础，定义了空间线目标的端点、内部、边界等概念，在此基础上提出一种描述空间线目标间拓扑关系完善的形式化模型—新九交模型，并在此基础上总结出空间线目标间拓扑关系的最小集，定义了6种线目标间的基本拓扑关系[8]。邓敏、李志林、李永礼主要研究了IR2中两个线目标间拓扑关系的描述和区分方法[9]。陈军、刘万增等在2006年提出线目标间复杂拓扑关系的分解—组合计算思路，并应用于国家1∶5万地图数据库更新工作，取得良好效果[10]。

1.2 空间方向关系描述

夏宇、朱欣焰等给出空间方向关系形式化描述方法的分类，阐述空间方向关系的形式化描述模型与表达方法[11]；郭薇、陈军给出基于点集拓扑学的三维拓扑空间关系形式化描述框架[12]；郭薇、陈军给出基于k-维伪流行拓扑的三维空间实体语义定义与形式化描述[13]；闫浩文、郭仁忠在2003年详细阐述基于Voronoi图的空间方向关系形式化描述模型[14]；赵玉梅、李成名等结合GIS中地理实体的时间特性，给出时间数学上的形式化描述，并对各时间表达间相互关系进行探讨与系统分析[15]；邓敏、张雪松等针对空间目标点集拓扑运算所得集合的非闭性，提出一种适合于Euler示性数计算的方法，建立一种形式化描述拓扑关系的Euler示性数模型[16]。

空间方向关系形式化描述方法是空间方向关系研究的重点。这方面的研究成果在相关领域中都有出现。Peuquet等提出一个判别二维空间内任意形状、大小和距离的多边形之间方向关系的三角化模型[17]；S.K.Chang等提出2D String模型用以表达符号图及空间目标间的空间关系，从而用于影像检索领域[18]；Papadias，D.等提出MBR 模型并用于空间目标间拓扑关系的检索[19]；闫浩文等进一步从理论上证明了运用Voronoi图表达空间方向关系的可行性，并建立基于Voronoi图的空间方向关系形式化描述模型[20]。邓敏、李志林等给出线目标间拓扑关系描述的四交模型，可有效表达线目标间拓扑关系的变化特征[21]。

2 GIS需求形式化描述发展

目前，国内外形式描述与验证的形式化方法与地理信息系统结合发展[22-28]，其趋势主要体现在以下4个方面：①地理信息概念的形式化定义;②地理信息功能计算模块形式化设计与验证;③地理信息软件系统需求的形式化描述与精化;④地理信息系统与其它系统接口的形式化描述与分析等。

针对图形、文本、表格等非形式化需求描述方式无法做到准确、一致、无二义性等要求，邵小东等提出地理信息系统需求形式化描述与验证方法。以现代烟草农业中基础设施规划子模块需求描述与验证为例,将现代烟草农业对地理信息系统真实需求归纳到预定义地理信息子问题框架,涉及需求分解、问题子框架组合等系列工程问题,对烟草地理信息需求形式化定义与描述具有典型示范意义[29-30]。

图1为现代烟草农业地理信息系统重复建设需求子问题框架模块。通过问题框架描述“选择烟田，与该烟田相连的水窖、水池、山坪塘等相关项目全部高亮显示，弹出该对象的属性信息，辅助系统使用人员分析是否存在重复建设的水窖、水池、山坪塘等相关项目”。

图1 重复建设问题框架描述图

a:SF!{type ‘water works equipment’，criteria ‘address=address of water works equipment’}[Y1]

b:CO!{AlphaNumber codes}[Y2]

c:PSM!{Point(p，x，y)，Location(o，p)，Type(o，t)，Address(o，a)}[Y3]

d:DF!{type ‘water works equipment’}[Y4]

e:PM!{AlphaNumber codes }[Y5]

f:PO!{identification of water works equipment within X meters}[Y6]

g:DF!{objects that are water works equipment}[Y7]

h:PSM!{Tobacco Field(tf，x，y)，Water works equipment(wwe，x，y)，Address(tf，a)}[Y8]

i:CO!{Identification of tobacco field}[Y9]

j:SF!{address of tobacco field that are not overlap}[Y10]

3 GIS接口形式化定义

现在我国GIS行业的发展如火如荼，GIS系统与MIS系统结合日益紧密。接口是相互独立系统之间的通信和交互，接口规格是对如何使用特定编程语言所书写的模块的精确描述。

GIS系统与MIS系统信息集成需要预留接口，定义规范的接口是项目需要与功能组件库之间有效集成的重要体现，非形式化、规范化的接口定义模糊了需要实现的功能体，一方面使得项目合作甲乙双方不能很好达到一致沟通与理解，另一方面不利于项目开发人员后续工作的展开，因此展开对GIS系统与MIS系统信息集成接口形式化描述研究显得至关重要。下面为某一GIS接口模块的Alloy语言描述：

module Tobacco/com

open util/relation

sig IID {}

sig Interface {

qi：IID-> lone Interface,

iids：set IID,

iidsKnown：IID,

reaches：Interface

}{

iidsKnown = dom(qi)

reaches = ran(qi)

}

sig Component {

interfaces：set Interface,

iids：set IID,

first，identity：interfaces,

eqs：set Component,

aggregates：set Component

}

fact defineEqs {

all c1，c2：Component |

c1->c2 in eqs <=> c1.identity = c2.identity

}

fact IdentityAxiom {

some unknown：IID | all c：Component |

all i：c.interfaces | unknown.(i.qi) = c.identity

}

fact ComponentProps {

all c：Component {

c.iids = c.interfaces.iids

all i：c.interfaces | all x：IID | x.(i.qi) in c.interfaces

}

}

sig LegalInterface extends Interface { }

fact { all i：LegalInterface | all x：i.iidsKnown | x in x.(i.qi).iids}

sig LegalComponent extends Component { }

fact { LegalComponent.interfaces in LegalInterface }

fact Reflexivity { all i：LegalInterface | i.iids in i.iidsKnown }

fact Symmetry { all i，j：LegalInterface | j in i.reaches => i.iids in j.iidsKnown }

fact Transitivity { all i，j：LegalInterface | j in i.reaches => j.iidsKnown in i.iidsKnown }

fact Aggregation {

no c：Component | c in c.^aggregates

all outer：Component | all inner：outer.aggregates |

(some inner.interfaces & outer.interfaces)

&& some o：outer.interfaces | all i：inner.interfaces-inner.first | all x：Component | (x.iids).(i.qi) = (x.iids).(o.qi)

}

4 结束语

随着软件应用日益广泛，软件规模越来越大，软件开发面临着规模复杂性、结构复杂性、环境复杂性、应用领域复杂性以及交流复杂性等特点，因此从理论上探讨程序正确性和软件可靠性问题推动对形式化方法的深入研究。从严格意义上说，地理信息系统工程从需求分析、规格说明、设计、编程、系统集成、测试、文档生成直至维护各阶段，都可采用严格的数学语言、具有精确的数学语义的形式化方法进行定义分析。因此，形式化方法结合地理信息系统工程研究有待进一步加强，这也必将成为形式化方法、形式化模型理论在地理信息系统综合研究领域的发展新方向。

[1]古天龙.软件开发的形式化方法[M].北京：高等教育出版社，2005．

[2]COHN A G，GOTTS N M.The ‘Egg-Yolk’ Representation of Regions with Indeterminate Boundaries[A].In：Burrough P A and Frank A U (ed)，Proceedings of GISDATA-Specialist Meeting on Spatial Objects with Undetermined Boundaries [C].London：Taylor & Francis，1996，171-187.

[3]LI ZHILIN，ZHAO RENLIANG，CHEN Jun.An Algebra Model for Spatial Relatons [A].Proceedings of the 3RD ISPRS Workshop on Dynamic and Multi-dimensional GIS [C]，Bangkok：[s.n.]，2001，170-177.

[4]EGENHOFER M，FRANZOSA R.Point-Set Topological Spatial Relations [J].International Journal of Geographical Information Systems，1991，5 (2)：161-174.

[5]EGENHOFER M，HERRING J.Categoring Binary Topological Relationships between Regions，Lines，and Points in Geographic Database [R].Oronoi：Technical report，Department of Surveying Engineering.University of Maine，Oronoi，ME，1991.

[6]邓敏，刘文宝，冯学智.GIS面目标间拓扑关系的形式化模型[J].测绘学报，2005，34(1):87-90．

[7]陈军.Voronoi动态空间数据模型[M].北京：测绘出版社，2002:63-70．

[8]张水舰，李永树.GIS 空间线目标间拓扑关系形式化描述模型[J].测绘科学技术学报，2009，26(4):292-295．

[9]邓敏，李志林，李永礼.GIS线目标间拓扑关系描述的层次方法[J].遥感学报，2007，11(3):311-317．

[10]陈军，刘万增，李志林，等.线目标间拓扑关系的细化计算方法[J].测绘学报，2006，35(8):256-260．

[11]夏宇，朱欣焰，李德仁，等.GIS空间方向关系形式化描述模型分析[J].测绘科学，2007，32(5):94-97．

[12]郭薇，陈军.基于点集拓扑学的三维拓扑空间关系形式化描述[J].测绘学报，1997，26(2):122-127．

[13]郭薇，陈军.基于流行拓扑的三维空间实体形式化描述[J].武汉测绘科技大学学报，1997，22(3):201-206．

[14]闫浩文，郭仁忠.空间方向关系形式化描述模型研究[J].测绘学报，2003，32(1):42-46．

[15]赵玉梅，李成名，靳奉祥.时态地理信息系统中时间的形式化定义[J].测绘通报，2003(3):19-30．

[16]邓敏，张雪松，林宗坚．拓扑关系形式化描述的Euler示性数模型[J].武汉大学学报：信息科学版，2004，29(10):873-876．

[17]D J PEUQUET，CIXIANG ZHANG.An algorithm to determine the directional relationship between arbitrarily-shaped polygons in the plane[M].Pattern Recognition，1987:65-74.

[18]S K CHANG，Q Y SHI，C W YAN.Iconic indexing by 2-D strings[M].IEEE Transactions on Pattern Analysis and Machine Intelligence，1987,5:413-428.

[19]Papadias，D.，Theodoridis，Y.，Sellis，T.，Egenhofer,M.Topological Relations in the World of Minimum Bounding Rectangles：a Study with R-trees.Proceedings of the ACM Conference on the Management of Data (SIGMOD)，San Jose，CA，ACM Press，1995.

[20]闫浩文，郭仁忠.用Voronoi图描述空间方向关系的理论依据[J]．武汉大学学报：信息科学版，2002，27(3):306-310．

[21]邓敏，李志林，李永礼，等.GIS 线目标间拓扑关系描述的交回模型[J].武汉大学学报：信息科学版，2006，31(11):945-948．

[22]石琳，张琼.人机交互策略在GIS软件用户界面设计中的研究[J].测绘与空间地理信息，2014，37(2)：165-167，170．

[23]毛曦.面向智慧城市的空间信息搜索引擎研究[J].测绘科学，2014，39(8)：33-35．

[24]王新量，李风光，祝若鑫.基于混合三维数据模型的二、三维联动研究[J].测绘工程，2014，23(4)：33-36．

[25]郭立群，王欣滔，王笑赤，等.海啸早期预警系统的一种本体式表达[J].测绘与空间地理信息，2014，37(7)：5-10．

[26]齐晓飞，王光霞，王富强，等.基于位置服务的语义位置建模研究[J].测绘科学，2014，39(5)：89-92．

[27]高翔，徐京华，王蕾，等.交通要素启发式多尺度表达技术方法探讨[J].测绘工程，2014，23(8)：62-65．

[28]张鑫，王莉.基于DLM和DCM的一体化模型发展[J].测绘与空间地理信息，2014，37(5)：116-119．

[29]邵小东，蒋样明，宋文峰，等.现代烟草农业地理信息系统需求形式化描述研究[J].中国烟草科学，2013，34(4):88-92.

[30]邵小东，郭继发，蒋样明，等.面向问题的GIS需求非形式化与形式化描述研究[J].测绘与空间地理信息，2012，35(1):6-9．

[责任编辑：张德福]

Application of formal descriptionto geographic Information System

SHAO Xiao-dong1,*，GUO Ji-fa2

(1.Honghe Tobacco Company of Yunnan Province，Mile 652399，China;2.College of Urban and Environmental Science，Tianjin Normal University,Tianjin 300387，China)

It presents the formal methods，theory and application to GIS，of which the formal description method is proposed in the spatial topological relations，distance and direction of the relationship between applications. The formal methods are analyzed on the application to the GIS engineering problem frame and application interface，namely on the precise and consistent definition of normalization，thus promoting information fusion，geographic information issues to be better understood and the GIS engineering development process quality.

formal methods;formal model;Geographic Information System;application development

2013-10-31；补充更新日期:2014-10-11

国家自然科学基金资助项目(41101352)

邵小东(1980-)，男，博士，工程师.

P208

：A

：1006-7949(2014)12-0017-04