Compositional Model Checking and Compositional Refinement Checking of Concurrent Reactive Systems
DOI:
Author:
Affiliation:

Clc Number:

Fund Project:

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

    Model checking and refinement checking are two approaches to formal verification, whose difficulties are due to the state explosion problem. As one of the proposed solutions to the problem, it is suggested to introduce compositionality in model checking and refinement checking based on the idea of divide-and-conquer, by which the verification task of the whole system is decomposed to several smaller subtasks on the subsystems. In a uniform framework, this paper surveys the approaches of compositional model checking and compositional refinement checking in a systematic way. From the perspective of module checking, the principle and verification strategies of the two compositional verification approaches are introduced. In addition, the complexities of various kinds of related problems are summarized and a comparison is made between compositional model checking and compositional refinement checking, which exposes the intrinsic relation between them. Finally, some trends are given for the future research.

    Reference
    Related
    Cited by
Get Citation

文艳军,王戟,齐治昌.并发反应式系统的组合模型检验与组合精化检验.软件学报,2007,18(6):1270-1281

Copy
Share
Article Metrics
  • Abstract:
  • PDF:
  • HTML:
  • Cited by:
History
  • Received:December 30,2004
  • Revised:July 05,2006
  • Adopted:
  • Online:
  • 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