| 基于原型验证系统的自稳定算法形式化验证 |
| |
| 引用本文： | 毛玲炤,邓玉欣.基于原型验证系统的自稳定算法形式化验证[J].上海交通大学学报,2009,43(6). |
| |
| 作者姓名： | 毛玲炤 邓玉欣 |
| |
| 作者单位： | 上海交通大学,计算机科学与工程系,上海,200240
|
| |
| 基金项目： | 国家重点基础研究发展规划(973计划)，国家自然科学基金 |
| |
| 摘 要： | 介绍了分布式系统的自稳定性以及原型验证系统(PVS),阐述了从形式化角度验证系统性质的方法.使用PVS对分布式系统及系统中的自稳定算法进行形式化描述和建模,并成功地证明了系统的自稳定性.同时,通过机械化的验证和分析结果,可以得出形式化证明的优势.
|
| 关 键 词： | 分布式系统 自稳定算法 形式化分析 原型验证系统 |
Formal Analysis of a Self-Stabilizing Algorithm Using Prototype Verification System Prototype Verification System |
| |
| MAO Ling-zhao,DENG Yu-xin.Formal Analysis of a Self-Stabilizing Algorithm Using Prototype Verification System Prototype Verification System[J].Journal of Shanghai Jiaotong University,2009,43(6). |
| |
| Authors: | MAO Ling-zhao DENG Yu-xin |
| |
| Abstract: | |
| |
| Keywords: | |
| 本文献已被 CNKI 万方数据 等数据库收录！ |
|
