中文摘要：

由于无线传感器网络（WSN）带来的新特点，需要开发更多区别于传统网络的路由协议。形式化方法Object—Z是建立在严密数学基础之上的开发方法，其形式化规约语言的测试和设计工作可以同时开始，适用于新网络、新算法的研究开发。文章提出了运用形式化方法Object—Z对flooding算法建模的方法。建模结果表明Object--Z适用于无线传感器网络的路由协议，并可实现对flooding算法的描述和验证。

英文摘要：

A new type of networks wireless sensor network introduces untraditional aspects which is different from existing network protocols. So it＇s necessary to develop more new routing protocols. Object--Z is based on rigorous mathematics, which is a development methodology suited to the development of new network and new algorithm. It presents a way to model flooding algorithm using Object--Z. The result of modeling indicates that Object--Z is suitable to routing algorithm of WSN, and it＇s feasible to specify and verify flooding algorithm.