2nd International ICST Conference on Scalable Information Systems

Research Article

A Compositional Symbolic Verification Framework for Concurrent Software

Download140 downloads
  • @INPROCEEDINGS{10.4108/infoscale.2007.906,
        author={Conghua Zhou},
        title={A Compositional Symbolic Verification Framework for Concurrent Software},
        proceedings={2nd International ICST Conference on Scalable Information Systems},
        proceedings_a={INFOSCALE},
        year={2010},
        month={5},
        keywords={model checking SAT abstract composition.},
        doi={10.4108/infoscale.2007.906}
    }
    
  • Conghua Zhou
    Year: 2010
    A Compositional Symbolic Verification Framework for Concurrent Software
    INFOSCALE
    ICST
    DOI: 10.4108/infoscale.2007.906
Conghua Zhou1,*
  • 1: School of Computer Science and Telecommunication Engineering, Jiangsu University No. 301 Xufu Road Zhenjiang, China, 212013
*Contact email: chzhou@mail.edu.cn

Abstract

For concurrent software systems state/event linear temporal logic SE-LTL is a specification language with high expressive power and the ability to reason about both states and events. Until now, SE-LTL model checking algorithm is still explicit. For SE-LTL we provide a SAT-based Bounded Model Checking procedure. We also present a framework for model checking concurrent software systems which integrates three powerful verification techniques, SAT-based Bounded Model Checking, counterexample-guided abstraction refinement and compositional reasoning. In the framework the abstraction and refinement steps are performed over each component separately, and the model checking step is symbolic.