计算机工程与设计
計算機工程與設計
계산궤공정여설계
COMPUTER ENGINEERING AND DESIGN
2010年
1期
118-121,136
,共5页
限界模型检测%一阶迁移系统%通道%验证算法%协议分析
限界模型檢測%一階遷移繫統%通道%驗證算法%協議分析
한계모형검측%일계천이계통%통도%험증산법%협의분석
bounded model checking%first order transition system%channel%verification algorithm%protocol analysis
为了简化在限界模型检测过程中模型的建立过程,给出了一种采用基于一阶迁移系统语言的模型建立方法,并在此一阶迁移系统语言中加入了通道的功能,增强了描述能力.然后在此基础上完成了一个以基于插值和k步归纳的限界验证算法为核心的模型检测工具(BMCF),最后利用该工具对常见的互斥协议,简单数据传输协议的性质进行了分析与验证.结果表明,利用该工具对系统进行建模具有方便直观的特点,并借助实现的验证算法能高效的检验性质的正确性,如果性质不成立工具还会给出反例提示.
為瞭簡化在限界模型檢測過程中模型的建立過程,給齣瞭一種採用基于一階遷移繫統語言的模型建立方法,併在此一階遷移繫統語言中加入瞭通道的功能,增彊瞭描述能力.然後在此基礎上完成瞭一箇以基于插值和k步歸納的限界驗證算法為覈心的模型檢測工具(BMCF),最後利用該工具對常見的互斥協議,簡單數據傳輸協議的性質進行瞭分析與驗證.結果錶明,利用該工具對繫統進行建模具有方便直觀的特點,併藉助實現的驗證算法能高效的檢驗性質的正確性,如果性質不成立工具還會給齣反例提示.
위료간화재한계모형검측과정중모형적건립과정,급출료일충채용기우일계천이계통어언적모형건립방법,병재차일계천이계통어언중가입료통도적공능,증강료묘술능력.연후재차기출상완성료일개이기우삽치화k보귀납적한계험증산법위핵심적모형검측공구(BMCF),최후이용해공구대상견적호척협의,간단수거전수협의적성질진행료분석여험증.결과표명,이용해공구대계통진행건모구유방편직관적특점,병차조실현적험증산법능고효적검험성질적정학성,여과성질불성립공구환회급출반례제시.
To simplify the modeling in the process of bounded model checking,a method of modeling based on first order transition system is presented,and channel function is added for enhancing description ability.A bounded model checker based on first order transition system language as input language,interpolation and k-induction as core verification algorithms(BMCF)is implemented,finally,properties of mutual exclusion protocoland simple data transfer protoeol are checked by it.As a result,the convenient and intuitive features of modeling are dcmonstrated by the tool,and the efficiency of property verification and counterexaraple generation function are shown by bounded model checking algorithms which are implemented in the tool.
