论文部分内容阅读
模型检测是通信顺序进程（communicating sequential processes,简称CSP）形式化验证的重要手段.当前,CSP模型检测方法基于操作语义,需将进程转化为迁移系统,进而提取语义模型,但转化过程较为复杂;待验证性质采用CSP语言进行描述,虽然有利于精炼检测（refinement checking）,但描述能力较弱,通用性不强.鉴于此,提出了一种新的CSP指称语义模型——关键迹模型（critical-trace model）及基于该指称语义模型的CSP模型检测方法,并证明了其验证的可