%0 Journal Article
%T Algorithmic Verification of Forward Correctability<br>前向可修正属性算术验证的研究
%A WU Hai-ling
%A ZHOU Cong-hua
%A JU Shi-guang
%A WANG Ji
%A <br>吴海玲
%A 周从华
%A 鞠时光
%A 王基
%J 计算机科学
%D 2011
%I 
%X 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.
%K Forward correctability
%K Information flow
%K Non-interference
%K Sate transition system<br>前向可修正属性，信息流，无干扰，状态转换系统
%U http://www.alljournals.cn/get_abstract_url.aspx?pcid=5B3AB970F71A803DEACDC0559115BFCF0A068CD97DD29835&cid=8240383F08CE46C8B05036380D75B607&jid=64A12D73428C8B8DBFB978D04DFEB3C1&aid=3310C84FD5AF166B186F96D8ACC62972&yid=9377ED8094509821&vid=16D8618C6164A3ED&iid=38B194292C032A66&sid=C3BF5C58156BEDF0&eid=331211A5F5616413&journal_id=1002-137X&journal_name=计算机科学&referenced_num=0&reference_num=18