并发反应式系统的组合模型检验与组合精化检验-软件工程和软件质量.PDF

ISSN 1000-9825, CODEN RUXUEW E-mail: jos@ Journal of Software , Vol.18, No.6, June 2007, pp.1270− 1281 DOI: 10.1360/jos181270 Tel/Fax: +86-10 © 2007 by Journal of Software . All rights reserved. ∗ 1 1,2+ 1 , , 1( , 410073) 2 ( , 410073) Compositional Model Checking and Compositional Refinement Checking of Concurrent Reactive Systems 1 1,2+ 1 WEN Yan-Jun , WANG Ji , QI Zhi-Chang 1(School of Computer, National University of Defense Technology, Changsha 410073, China) 2(National Laboratory for Parallel and Distributed Processing, Changsha 410073, China) + Corresponding author: Phn: +86-731-4573637, E-mail: wj@ Wen YJ, Wang J, Qi ZC. Compositional model checking and compositional refinement checking of concurrent reactive systems. Journal of Software, 2007,18(6):1270−1281. /1000-9825/18/ 1270.htm 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 m