形式化描述方法在地理信息系統中應用綜述

邵小東，郭繼發

(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