Refinement Checking Based on Simulation Relations
Author:
Affiliation:

Clc Number:

Fund Project:

National Natural Science Foundation of China (61103044, U1509214); Natural Science Foundation of Zhejiang Province of China (LQ15E050006, LY16F020035)

  • Article
  • |
  • Figures
  • |
  • Metrics
  • |
  • Reference
  • |
  • Related
  • |
  • Cited by
  • |
  • Materials
  • |
  • Comments
    Abstract:

    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.

    Reference
    Related
    Cited by
Get Citation

王婷,陈铁明,刘杨.基于模拟关系的精化检测方法.软件学报,2016,27(3):580-592

Copy
Share
Article Metrics
  • Abstract:
  • PDF:
  • HTML:
  • Cited by:
History
  • Received:July 15,2015
  • Revised:October 20,2015
  • Adopted:
  • Online: January 06,2016
  • Published:
You are the firstVisitors
Copyright: Institute of Software, Chinese Academy of Sciences Beijing ICP No. 05046678-4
Address:4# South Fourth Street, Zhong Guan Cun, Beijing 100190,Postal Code:100190
Phone:010-62562563 Fax:010-62562533 Email:jos@iscas.ac.cn
Technical Support:Beijing Qinyun Technology Development Co., Ltd.

Beijing Public Network Security No. 11040202500063