邵小東，郭繼發(fā)

(1.云南省煙草公司紅河州公司，云南 彌勒 652399；2.天津師范大學(xué) 城市與環(huán)境科學(xué)學(xué)院，天津 300387)

形式化描述方法在地理信息系統(tǒng)中應(yīng)用綜述

邵小東1，郭繼發(fā)2

(1.云南省煙草公司紅河州公司，云南 彌勒 652399；2.天津師范大學(xué) 城市與環(huán)境科學(xué)學(xué)院，天津 300387)

總結(jié)形式化理論與地理信息系統(tǒng)的應(yīng)用情況，闡述形式化描述方法在空間拓?fù)潢P(guān)系、距離關(guān)系與方向關(guān)系等方面的應(yīng)用。文中提出形式化方法在地理信息系統(tǒng)問題框架描述與多系統(tǒng)接口描述中的應(yīng)用，即通過形式化方法精確一致的規(guī)格化描述定義，促進(jìn)對地理信息領(lǐng)域問題的更好理解，促進(jìn)信息融合，提高地理信息系統(tǒng)開發(fā)質(zhì)量。

形式化方法；形式化模型；地理信息系統(tǒng)；應(yīng)用綜述

形式化方法是基于嚴(yán)密的、數(shù)學(xué)上的形式機(jī)制的系統(tǒng)研究方法?？陀^地講，有了數(shù)學(xué)的應(yīng)用，就有了形式化方法。從廣義角度講，形式化方法是軟件開發(fā)過程中規(guī)格、設(shè)計(jì)及實(shí)現(xiàn)的系統(tǒng)工程方法；狹義上，形式化方法是軟件規(guī)格和驗(yàn)證的方法。因此，形式化方法又分為形式化規(guī)格和形式化驗(yàn)證法方法[1]。

1 形式化與地理信息系統(tǒng)結(jié)合應(yīng)用

目前，縱觀國內(nèi)外所刊文獻(xiàn)資料，形式化描述在空間信息系統(tǒng)方面的應(yīng)用主要集中在空間拓?fù)潢P(guān)系、距離關(guān)系與方向關(guān)系等方面?？臻g關(guān)系描述的基本任務(wù)是以數(shù)學(xué)邏輯的方法區(qū)分不同的空間關(guān)系，給出形式化的描述。其意義在于澄清不同用戶關(guān)于空間關(guān)系的語義，為空間關(guān)系判斷、推理，構(gòu)造空間查詢語言和空間分析提供形式化工具。

1.1 線面拓?fù)潢P(guān)系描述

針對面目標(biāo)間的拓?fù)潢P(guān)系描述，已建立一些形式化描述模型，如基于空間邏輯的RCC模型(Region Connection Calculus)[2]、空間代數(shù)模型[3]，以及四交模型[4]和九交模型[5]等。鄧敏、劉文寶等建立一種GIS中面目標(biāo)間拓?fù)潢P(guān)系形式化描述和區(qū)分的廣義模型[6]。

針對線目標(biāo)間拓?fù)潢P(guān)系的描述，建立的一些形式化描述模型都有一定的空間目標(biāo)間拓?fù)潢P(guān)系表達(dá)能力，如九交模型能區(qū)分線與線之間的33種拓?fù)潢P(guān)系[7]。張水艦、李永樹以點(diǎn)集拓?fù)鋵W(xué)基本理論為基礎(chǔ)，定義了空間線目標(biāo)的端點(diǎn)、內(nèi)部、邊界等概念，在此基礎(chǔ)上提出一種描述空間線目標(biāo)間拓?fù)潢P(guān)系完善的形式化模型—新九交模型，并在此基礎(chǔ)上總結(jié)出空間線目標(biāo)間拓?fù)潢P(guān)系的最小集，定義了6種線目標(biāo)間的基本拓?fù)潢P(guān)系[8]。鄧敏、李志林、李永禮主要研究了IR2中兩個線目標(biāo)間拓?fù)潢P(guān)系的描述和區(qū)分方法[9]。陳軍、劉萬增等在2006年提出線目標(biāo)間復(fù)雜拓?fù)潢P(guān)系的分解—組合計(jì)算思路，并應(yīng)用于國家1∶5萬地圖數(shù)據(jù)庫更新工作，取得良好效果[10]。

1.2 空間方向關(guān)系描述

夏宇、朱欣焰等給出空間方向關(guān)系形式化描述方法的分類，闡述空間方向關(guān)系的形式化描述模型與表達(dá)方法[11]；郭薇、陳軍給出基于點(diǎn)集拓?fù)鋵W(xué)的三維拓?fù)淇臻g關(guān)系形式化描述框架[12]；郭薇、陳軍給出基于k-維偽流行拓?fù)涞娜S空間實(shí)體語義定義與形式化描述[13]；閆浩文、郭仁忠在2003年詳細(xì)闡述基于Voronoi圖的空間方向關(guān)系形式化描述模型[14]；趙玉梅、李成名等結(jié)合GIS中地理實(shí)體的時間特性，給出時間數(shù)學(xué)上的形式化描述，并對各時間表達(dá)間相互關(guān)系進(jìn)行探討與系統(tǒng)分析[15]；鄧敏、張雪松等針對空間目標(biāo)點(diǎn)集拓?fù)溥\(yùn)算所得集合的非閉性，提出一種適合于Euler示性數(shù)計(jì)算的方法，建立一種形式化描述拓?fù)潢P(guān)系的Euler示性數(shù)模型[16]。

空間方向關(guān)系形式化描述方法是空間方向關(guān)系研究的重點(diǎn)。這方面的研究成果在相關(guān)領(lǐng)域中都有出現(xiàn)。Peuquet等提出一個判別二維空間內(nèi)任意形狀、大小和距離的多邊形之間方向關(guān)系的三角化模型[17]；S.K.Chang等提出2D String模型用以表達(dá)符號圖及空間目標(biāo)間的空間關(guān)系，從而用于影像檢索領(lǐng)域[18]；Papadias，D.等提出MBR 模型并用于空間目標(biāo)間拓?fù)潢P(guān)系的檢索[19]；閆浩文等進(jìn)一步從理論上證明了運(yùn)用Voronoi圖表達(dá)空間方向關(guān)系的可行性，并建立基于Voronoi圖的空間方向關(guān)系形式化描述模型[20]。鄧敏、李志林等給出線目標(biāo)間拓?fù)潢P(guān)系描述的四交模型，可有效表達(dá)線目標(biāo)間拓?fù)潢P(guān)系的變化特征[21]。

2 GIS需求形式化描述發(fā)展

目前，國內(nèi)外形式描述與驗(yàn)證的形式化方法與地理信息系統(tǒng)結(jié)合發(fā)展[22-28]，其趨勢主要體現(xiàn)在以下4個方面：①地理信息概念的形式化定義;②地理信息功能計(jì)算模塊形式化設(shè)計(jì)與驗(yàn)證;③地理信息軟件系統(tǒng)需求的形式化描述與精化;④地理信息系統(tǒng)與其它系統(tǒng)接口的形式化描述與分析等。

針對圖形、文本、表格等非形式化需求描述方式無法做到準(zhǔn)確、一致、無二義性等要求，邵小東等提出地理信息系統(tǒng)需求形式化描述與驗(yàn)證方法。以現(xiàn)代煙草農(nóng)業(yè)中基礎(chǔ)設(shè)施規(guī)劃子模塊需求描述與驗(yàn)證為例,將現(xiàn)代煙草農(nóng)業(yè)對地理信息系統(tǒng)真實(shí)需求歸納到預(yù)定義地理信息子問題框架,涉及需求分解、問題子框架組合等系列工程問題,對煙草地理信息需求形式化定義與描述具有典型示范意義[29-30]。

圖1為現(xiàn)代煙草農(nóng)業(yè)地理信息系統(tǒng)重復(fù)建設(shè)需求子問題框架模塊。通過問題框架描述“選擇煙田，與該煙田相連的水窖、水池、山坪塘等相關(guān)項(xiàng)目全部高亮顯示，彈出該對象的屬性信息，輔助系統(tǒng)使用人員分析是否存在重復(fù)建設(shè)的水窖、水池、山坪塘等相關(guān)項(xiàng)目”。

圖1 重復(fù)建設(shè)問題框架描述圖

a:SF!{type ‘water works equipment’，criteria ‘a(chǎn)ddress=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接口形式化定義

現(xiàn)在我國GIS行業(yè)的發(fā)展如火如荼，GIS系統(tǒng)與MIS系統(tǒng)結(jié)合日益緊密。接口是相互獨(dú)立系統(tǒng)之間的通信和交互，接口規(guī)格是對如何使用特定編程語言所書寫的模塊的精確描述。

GIS系統(tǒng)與MIS系統(tǒng)信息集成需要預(yù)留接口，定義規(guī)范的接口是項(xiàng)目需要與功能組件庫之間有效集成的重要體現(xiàn)，非形式化、規(guī)范化的接口定義模糊了需要實(shí)現(xiàn)的功能體，一方面使得項(xiàng)目合作甲乙雙方不能很好達(dá)到一致溝通與理解，另一方面不利于項(xiàng)目開發(fā)人員后續(xù)工作的展開，因此展開對GIS系統(tǒng)與MIS系統(tǒng)信息集成接口形式化描述研究顯得至關(guān)重要。下面為某一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 結(jié)束語

隨著軟件應(yīng)用日益廣泛，軟件規(guī)模越來越大，軟件開發(fā)面臨著規(guī)模復(fù)雜性、結(jié)構(gòu)復(fù)雜性、環(huán)境復(fù)雜性、應(yīng)用領(lǐng)域復(fù)雜性以及交流復(fù)雜性等特點(diǎn)，因此從理論上探討程序正確性和軟件可靠性問題推動對形式化方法的深入研究。從嚴(yán)格意義上說，地理信息系統(tǒng)工程從需求分析、規(guī)格說明、設(shè)計(jì)、編程、系統(tǒng)集成、測試、文檔生成直至維護(hù)各階段，都可采用嚴(yán)格的數(shù)學(xué)語言、具有精確的數(shù)學(xué)語義的形式化方法進(jìn)行定義分析。因此，形式化方法結(jié)合地理信息系統(tǒng)工程研究有待進(jìn)一步加強(qiáng)，這也必將成為形式化方法、形式化模型理論在地理信息系統(tǒng)綜合研究領(lǐng)域的發(fā)展新方向。

[1]古天龍.軟件開發(fā)的形式化方法[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，F(xiàn)RANZOSA 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]鄧敏，劉文寶，馮學(xué)智.GIS面目標(biāo)間拓?fù)潢P(guān)系的形式化模型[J].測繪學(xué)報，2005，34(1):87-90．

[7]陳軍.Voronoi動態(tài)空間數(shù)據(jù)模型[M].北京：測繪出版社，2002:63-70．

[8]張水艦，李永樹.GIS 空間線目標(biāo)間拓?fù)潢P(guān)系形式化描述模型[J].測繪科學(xué)技術(shù)學(xué)報，2009，26(4):292-295．

[9]鄧敏，李志林，李永禮.GIS線目標(biāo)間拓?fù)潢P(guān)系描述的層次方法[J].遙感學(xué)報，2007，11(3):311-317．

[10]陳軍，劉萬增，李志林，等.線目標(biāo)間拓?fù)潢P(guān)系的細(xì)化計(jì)算方法[J].測繪學(xué)報，2006，35(8):256-260．

[11]夏宇，朱欣焰，李德仁，等.GIS空間方向關(guān)系形式化描述模型分析[J].測繪科學(xué)，2007，32(5):94-97．

[12]郭薇，陳軍.基于點(diǎn)集拓?fù)鋵W(xué)的三維拓?fù)淇臻g關(guān)系形式化描述[J].測繪學(xué)報，1997，26(2):122-127．

[13]郭薇，陳軍.基于流行拓?fù)涞娜S空間實(shí)體形式化描述[J].武漢測繪科技大學(xué)學(xué)報，1997，22(3):201-206．

[14]閆浩文，郭仁忠.空間方向關(guān)系形式化描述模型研究[J].測繪學(xué)報，2003，32(1):42-46．

[15]趙玉梅，李成名，靳奉祥.時態(tài)地理信息系統(tǒng)中時間的形式化定義[J].測繪通報，2003(3):19-30．

[16]鄧敏，張雪松，林宗堅(jiān)．拓?fù)潢P(guān)系形式化描述的Euler示性數(shù)模型[J].武漢大學(xué)學(xué)報：信息科學(xué)版，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圖描述空間方向關(guān)系的理論依據(jù)[J]．武漢大學(xué)學(xué)報：信息科學(xué)版，2002，27(3):306-310．

[21]鄧敏，李志林，李永禮，等.GIS 線目標(biāo)間拓?fù)潢P(guān)系描述的交回模型[J].武漢大學(xué)學(xué)報：信息科學(xué)版，2006，31(11):945-948．

[22]石琳，張瓊.人機(jī)交互策略在GIS軟件用戶界面設(shè)計(jì)中的研究[J].測繪與空間地理信息，2014，37(2)：165-167，170．

[23]毛曦.面向智慧城市的空間信息搜索引擎研究[J].測繪科學(xué)，2014，39(8)：33-35．

[24]王新量，李風(fēng)光，祝若鑫.基于混合三維數(shù)據(jù)模型的二、三維聯(lián)動研究[J].測繪工程，2014，23(4)：33-36．

[25]郭立群，王欣滔，王笑赤，等.海嘯早期預(yù)警系統(tǒng)的一種本體式表達(dá)[J].測繪與空間地理信息，2014，37(7)：5-10．

[26]齊曉飛，王光霞，王富強(qiáng)，等.基于位置服務(wù)的語義位置建模研究[J].測繪科學(xué)，2014，39(5)：89-92．

[27]高翔，徐京華，王蕾，等.交通要素啟發(fā)式多尺度表達(dá)技術(shù)方法探討[J].測繪工程，2014，23(8)：62-65．

[28]張鑫，王莉.基于DLM和DCM的一體化模型發(fā)展[J].測繪與空間地理信息，2014，37(5)：116-119．

[29]邵小東，蔣樣明，宋文峰，等.現(xiàn)代煙草農(nóng)業(yè)地理信息系統(tǒng)需求形式化描述研究[J].中國煙草科學(xué)，2013，34(4):88-92.

[30]邵小東，郭繼發(fā)，蔣樣明，等.面向問題的GIS需求非形式化與形式化描述研究[J].測繪與空間地理信息，2012，35(1):6-9．

[責(zé)任編輯：張德福]

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；補(bǔ)充更新日期:2014-10-11

國家自然科學(xué)基金資助項(xiàng)目(41101352)

邵小東(1980-)，男，博士，工程師.

P208

：A

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