中文摘要：

介绍了分布式系统的自稳定性以及原型验证系统（PVS）,阐述了从形式化角度验证系统性质的方法.使用PVS对分布式系统及系统中的自稳定算法进行形式化描述和建模,并成功地证明了系统的自稳定性.同时,通过机械化的验证和分析结果,可以得出形式化证明的优势.

英文摘要：

PVS（prototype verification system） provides an integrated environment for developing and verifying formal specification. This paper introduced self-stabilization of distributed systems and PVS. Formalization of a self-stabilizing algorithm was presented and some properties of the system were formally verified using PVS.