自主卫星移动通信系统需要管理大量的信道资源和业务流程,其网络协议层具有很高的复杂度。为了对其进行工程实现,对协议的形式化技术进行研究,给出一种基于有限状态机的网络协议实现和一致性测试方法,并通过自主卫星移动通信网络协议中移动性管理子层的开发和测试进行验证。一致性测试的结果表明,上述方法能够有效保证协议层实现的正确性和完备性。