| 前向可修正属性算术验证的研究 |
| |
| 引用本文： | 吴海玲,周从华,鞠时光,王基.前向可修正属性算术验证的研究[J].计算机科学,2011,38(3):97-102. |
| |
| 作者姓名： | 吴海玲 周从华 鞠时光 王基 |
| |
| 作者单位： | 1. 江苏大学计算机科学与通信工程学院,镇江,212013
2. 镇江市地方税务局,镇江,212003 |
| |
| 基金项目： | 本文受国家自然科学基金(60773049),江苏大学高级人才科研启动基金(07JDG014),江苏省高校自然科学基金(08KJD520015),教育部博士点基金(20093227110005)资助。 |
| |
| 摘 要： | 目前验证前向可修正属性的"展开方法"是不完备的,即当"展开定理"的局部条件不满足时,不能判断出系统不满足前向可修正属性.为此,提出一种基于状态转换系统的前向可修正属性验证方法,该方法将前向可修正属性的验证归约为可达性问题,进而可借助可达性检测技术完成属性的验证.该方法是完备的,且当属性不成立时,可以给出使属性失效的反例...
|
| 关 键 词： | 前向可修正属性 信息流 无干扰 状态转换系统 |
Algorithmic Verification of Forward Correctability |
| |
| WU Hai-ling,ZHOU Cong-hu,JU Shi-guang,WANG Ji.Algorithmic Verification of Forward Correctability[J].Computer Science,2011,38(3):97-102. |
| |
| Authors: | WU Hai-ling ZHOU Cong-hu JU Shi-guang WANG Ji |
| |
| Affiliation: | (School of Computer Science and Telecommunication Engineering,Jiangsu University,Zhenjiang 212013,China);(Zhenjiang Municipal Local Taxation Bureau,Zhenjiang 212003,China) |
| |
| Abstract: | Due to the incompleteness of the "Unwinding Theorem",a system can't be judged to fail to satisfy the forward correctability, when some local conditions of "Unwinding Theorem" are not satisfied. This paper proposed an algorithmic verification technique to check the forward correctability based on the state transition system. The technique reduces forward correctability checking to the reachability problem and the reduction enables us to use the reachability checking technique to perform forward correctability checking. Our method is complete and it can give a counter-examples to control and eliminate the illegal information flow when a system fails to satisfy the forward correctability. Finally,Disk-arm Convert Channel illustrates the effectiveness and practicality. |
| |
| Keywords: | Forward correctability Information flow Non-interference Sate transition system |
| 本文献已被 万方数据 等数据库收录！ |
|
点击此处可从《计算机科学》下载全文 |
|
