主页期刊介绍编委会编辑部服务介绍道德声明在线审稿编委办公编辑办公English
     
在线出版
各期目录
纸质出版
分辑系列
论文检索
论文排行
综述文章
专刊文章
美文分享
各期封面
E-mail Alerts
RSS
旧版入口
中国科学院软件研究所
  
投稿指南 问题解答 下载区 收费标准 在线投稿
赵岭忠,翟仲毅,钱俊彦,郭云川.基于关键迹和ASP的CSP模型检测.软件学报,2015,26(10):2521-2544
基于关键迹和ASP的CSP模型检测
Model Checking CSP Based on ASP and Critical-Trace Model of CSP
投稿时间:2013-09-10  修订日期:2014-09-29
DOI:10.13328/j.cnki.jos.004738
中文关键词:  模型检测  通信顺序进程  关键迹模型  线性时态逻辑  回答集程序设计
英文关键词:model checking  communicating sequential process  critical-trace model  linear temporal logic  answer set programming
基金项目:国家自然科学基金(61262008,61100186);广西自然科学基金(2013GXNSFBA019267);武汉大学软件工程国家重点实验室开放基金(SKLSE20100806);广西教育厅重点项目;广西高等学校高水平创新团队及卓越学者计划;广西可信软件重点实验室基金(kx201113,kx201415);桂林电子科技大学创新团队资助项目
作者单位E-mail
赵岭忠 软件工程国家重点实验室武汉大学, 湖北 武汉 430072
广西可信软件重点实验室桂林电子科技大学, 广西 桂林 541004 
 
翟仲毅 广西可信软件重点实验室桂林电子科技大学, 广西 桂林 541004  
钱俊彦 广西可信软件重点实验室桂林电子科技大学, 广西 桂林 541004 qjy2000@gmail.com 
郭云川 中国科学院 信息工程研究所, 北京 100093  
摘要点击次数: 2182
全文下载次数: 1961
中文摘要:
      模型检测是通信顺序进程(communicating sequential processes,简称CSP)形式化验证的重要手段.当前, CSP模型检测方法基于操作语义,需将进程转化为迁移系统,进而提取语义模型,但转化过程较为复杂;待验证性质采用CSP语言进行描述,虽然有利于精炼检测(refinement checking),但描述能力较弱,通用性不强.鉴于此,提出了一种新的CSP指称语义模型——关键迹模型(critical-trace model)及基于该指称语义模型的CSP模型检测方法,并证明了其验证的可靠性,避免了上述问题.关键迹模型采用递归策略计算,待验证性质采用线性时态逻辑(linear temporal logic,简称LTL)描述.基于回答集程序设计(answer set programming,简称ASP)实现了关键迹模型的自动生成及LTL的自动验证,并开发了一个CSP模型检测原型系统——T_ASP.实验结果表明:与类似系统相比,该系统的描述能力更强,验证结果的准确性更高,且可同时验证多条性质,在性质不满足时还可提供多条反例.
英文摘要:
      Model checking is a mainstream method for formal verification of communicating sequential processes (CSP). Existing CSP model checkers are based on operational semantics, which need to translate processes into a label transition system, and to extract the semantic model based on the system. The conversion process is complex. Moreover, in most CSP model checkers, the properties to be verified are described by CSP, which is helpful for refinement checking, but at the same time leads to limited description power and weak generality. To address these issues, a new denotational semantic model of CSP, critical-trace model, is proposed and proved to be reliable for model checking CSP. Based on this model, a framework for model checking CSP is established to allow critical-trace model to be constructed inductively from the traces of its components, and properties to be specified by linear temporal logic (LTL), a universal property specification language. In addition, automatic mechanisms for generating critical-trace model and verifying LTL formulas are implemented with answer set programming (ASP). Finally, the two mechanisms are integrated into a CSP model checker T_ASP. Compared with the similar systems developed previously, experimental results indicate a higher ability of the proposed system to describe CSP processes and higher verification accuracy. Furthermore, T_ASP checks multiple properties in one execution of the system. When a property is not satisfied, the system also returns counterexamples for the property.
HTML  下载PDF全文  查看/发表评论  下载PDF阅读器
 

京公网安备 11040202500064号

主办单位:中国科学院软件研究所 中国计算机学会 京ICP备05046678号-4
编辑部电话:+86-10-62562563 E-mail: jos@iscas.ac.cn
Copyright 中国科学院软件研究所《软件学报》版权所有 All Rights Reserved
本刊全文数据库版权所有,未经许可,不得转载,本刊保留追究法律责任的权利