%0 Journal Article
%T 传值进程模型检测中诊断信息的生成
%A 刘剑？
%A 林惠民？
%J 软件学报
%P 1-8
%D 2003
%X 诊断信息自动生成是模型检测方法的基本特征之一,对分析和排错具有重要的意义.讨论了传值进程模型检测中诊断信息的生成问题.引入了两种诊断信息的表示结构:证明图和示例;提出了两种诊断信息构造算法.所采用的方法是从检测过程保存的依赖信息中抽取证明图和示例,这样可以继承已有的信息,从而减少计算量.相应的算法已经实现并用实例作了分析测试.实验结果表明该方法是有效的.
%K 进程代数
%K 模型检测
%K 证明图
%K 示例
%K 诊断生成
%U http://www.jos.org.cn/ch/reader/view_abstract.aspx?file_no=20030101&flag=1