As　an　important　value-added　function　for　GIS　service,　GIS　service　chain　provides　the　application　foundation　for　reusing　and　automation　composition　GIS　services.　An　important　issue　for　realizing　the　value-added　service　is　ensuring　the　operation　results　of　GIS　service　chain　meet　the　user　needs,　so　it　needs　to　verify　the　correctness　of　GIS　service　chain.　This　paper　introduces　the　equivalence　theory　of　Pi-calculus.　A　practical　GIS　service　chain　formal　model　is　established　using　Pi-calculus.　The　validity　of　GIS　service　chain　model　and　whether　it　meets　the　need　are　verified　using　the　formal　tools.　©　(2013)　Trans　Tech　Publications,　Switzerland.