用模块模型检查的方法来证明进程的正则网络的若干经验

提供了一个使用同步描述性语言ＬＵＳＴＲＥ的例子，这个例子是关于使用此语言来描述，说明和验证一个资源协调器（这是一种正则的网络硬件设备）程序及性质都可以用ＬＵＳＴＲＥ来表达的事实可以被用来作归纳验证，验证可通过模型检查来进行。