中文摘要：

BitTorrent（BT）是基于Peer-to—Peer（P2P）技术的比较流行文件共享软件，BTprotocol是其相关软件实现的一个基本协议．本文对BT协议进行深入的分析，采用有限状态机（FSM，Finite State Machine）对BT协议进行形式化建模，描述了正常的共享流程及部分异常处理．然后使用UIO方法生成了BT协议基于FSM模型的一致性测试序列，包括各个状态的UIO序列及各个变迁的测试序列，最后是本文的结论及下一步将要做的研究工作．

英文摘要：

BitTorrent（BT） is a popular software which is based on Peer-to-Peer （P2P）technology to support file sharing. BT protocol is a basic peer-to-peer protocol to all BT implementations. In this paper, BT protocol is deeply analyzed and its formal model is constructed with finite state machine （FSM） . The model discribes not only the formal sharing flow but also the part exception process. Whereafter the UIO method is chosen to generate the conformance test sequences including the UIO sequence of each state and test sequence of each transition. Finally, the conclusion and the research work in the future are presented.