主页期刊介绍编委会编辑部服务介绍道德声明在线审稿编委办公编辑办公English
2018-2019年专刊出版计划 微信服务介绍 最新一期:2018年第12期
     
在线出版
各期目录
纸质出版
分辑系列
论文检索
论文排行
综述文章
专刊文章
美文分享
各期封面
E-mail Alerts
RSS
旧版入口
中国科学院软件研究所
  
投稿指南 问题解答 下载区 收费标准 在线投稿
王婷,陈铁明,刘杨.基于模拟关系的精化检测方法.软件学报,2016,27(3):580-592
基于模拟关系的精化检测方法
Refinement Checking Based on Simulation Relations
投稿时间:2015-07-15  修订日期:2015-10-20
DOI:10.13328/j.cnki.jos.004982
中文关键词:  精化检测  模拟  failures  divergence  时间自动机
英文关键词:refinement checking  simulation  failure  divergence  timed automata
基金项目:国家自然科学基金(61103044,U1509214);浙江省自然科学基金(LQ15E050006,LY16F020035)
作者单位E-mail
王婷 浙江工业大学计算机科学与技术学院, 浙江 杭州 310023  
陈铁明 浙江工业大学计算机科学与技术学院, 浙江 杭州 310023 tmchen@zjut.edu.cn 
刘杨 School of Computer Engineering, Nanyang Technological University, Singapore 639798, Singapore  
摘要点击次数: 2179
全文下载次数: 1331
中文摘要:
      精化检测是一种重要的形式化验证方法,将系统实现和性质规约用相同的形式化语言进行建模,如能证明两者间存在某种精化关系,且该关系能够维持性质,可得出系统实现满足性质规约.为验证不同类型的系统性质,traces,stable failures和failures-divergence精化检测方法已被提出.精化检测算法依赖于子集构造,因而其面临状态空间爆炸问题.近年来,已有学者针对NFA语言包含问题提出了基于模拟关系的状态空间消减方法,极大地提高了算法的性能,且该方法能够直接用于traces精化检测.在此基础上,提出了基于模拟关系的stable failures和failuresdivergence精化检测方法.此外,还将精化检测扩展到了时间系统的验证中,提出了基于模拟关系的时间自动机traces精化检测方法.实验结果表明,基于模拟关系的算法效率有很大提高.
英文摘要:
      Refinement checking is an important method in formal verification to convey a refinement relationship between an implementation model and a specification model in the same language.If the specification satisfies certain property and the refinement relationship is strong enough to preserve the property, then implementation satisfies the property.Refinement checking was developed in order to verify different kinds of properties, traces, stables failures and failures/divergence.Refinement checking often relies on the subset construction, thus suffers from state space explosion.Recently, some researchers proposed a simulation based approach for solving the language inclusion problem of NFA, which outperforms the previous methods significantly and can be directly used in traces refinement checking.Base on this advancement, this work further proposes stable failures and failures-divergence refinement checking algorithms based on simulation relations.In addition, this work also extends the idea of trace refinement checking to timed systems, and proposes timed automata traces refinement checking based on simulation relations.Experimental results confirm the efficiency of the presented approaches.
HTML  下载PDF全文  查看/发表评论  下载PDF阅读器
 

京公网安备 11040202500064号

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