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

• 作者: 孙文圣
• 来源期刊: 抗恶劣环境计算机
• 学科: 工学
• 关键词: 正则网络 模块 模型检查 LUSTRE语言 操作系统
• 年，卷（期）: 1996,（4）
• 页码范围: 15-27
• 页数: 13页
• 分类号: TP316

摘要

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