%0 Journal Article
%T Compositional Model Checking and Compositional Refinement Checking of Concurrent Reactive Systems<br>并发反应式系统的组合模型检验与组合精化检验
%A WEN Yan-Jun
%A WANG Ji
%A QI Zhi-Chang
%A <br>文艳军
%A 王戟
%A 齐治昌
%J 软件学报
%D 2007
%I 
%X 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.
%K model checking
%K refinement checking
%K compositional model checking
%K compositional refinement checking
%K state explosion problem
%K module checking<br>模型检验
%K 精化检验
%K 组合模型检验
%K 组合精化检验
%K 状态爆炸问题
%K 模块检验
%U http://www.alljournals.cn/get_abstract_url.aspx?pcid=5B3AB970F71A803DEACDC0559115BFCF0A068CD97DD29835&cid=8240383F08CE46C8B05036380D75B607&jid=7735F413D429542E610B3D6AC0D5EC59&aid=D443669D1FC5F417&yid=A732AF04DDA03BB3&vid=13553B2D12F347E8&iid=B31275AF3241DB2D&sid=A5CB84B03418407D&eid=4CBFE0C7AFFA0387&journal_id=1000-9825&journal_name=软件学报&referenced_num=2&reference_num=35