%0 Journal Article
%T Diagnostic Information Generation in Model Checking Value-Passing Processes<br>传值进程模型检测中诊断信息的生成
%A LIU Jian
%A LIN Hui-Min
%A <br>刘剑
%A 林惠民
%J 软件学报
%D 2003
%I 
%X Automatic diagnostic information generation is one of the remarkable advantages of model checking methods. It is very important to understand the reason for the failure and fix the problem. In this paper, how to generate effective diagnosis in model checking value-passing processes is discussed. Two diagnostic forms, proof graph and witness, are defined. Moreover, algorithms are proposed to construct them from the search states space in model checking process. By this way, useful diagnoses are generated from the existing information by less calculation. Besides above, the algorithms have been implemented and used to analyze several cases. The experimental results show that this method is efficient.
%K process algebra
%K model checking
%K proof graph
%K witness
%K diagnosis generation<br>传值进程
%K 模型检测
%K 诊断信息
%K 进程代数
%K 证明图
%K 示例
%K 算法
%K 计算机
%U http://www.alljournals.cn/get_abstract_url.aspx?pcid=5B3AB970F71A803DEACDC0559115BFCF0A068CD97DD29835&cid=8240383F08CE46C8B05036380D75B607&jid=7735F413D429542E610B3D6AC0D5EC59&aid=E8383B7AD8A561E4&yid=D43C4A19B2EE3C0A&vid=F3583C8E78166B9E&iid=CA4FD0336C81A37A&sid=CA4FD0336C81A37A&eid=5D311CA918CA9A03&journal_id=1000-9825&journal_name=软件学报&referenced_num=8&reference_num=10