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

  • Article
  • | |
  • Metrics
  • |
  • Reference [35]
  • |
  • Related
  • |
  • Cited by
  • | |
  • 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
    [1]Browne A,de Alfaro L,Manna Z,Sipma HB,Uribe TE.Diagram-Based formalisms for the verification of reactive systems.In:Proc.of the CADE-13:Workshop on Visual Reasoning.Springer-Verlag,1996.
    [2]Thomas W.Languages,automata,and logic.In:Rozenberg G,Salomaa A,eds.Handbook of Formal Languages,Vol.3:Beyond Words.New York:Springer-Verlag,1997.389-455.
    [3]Lin H,Zhang W.Model checking:Theories,techniques and applications.Chinese Journal of Electronics,2002,30(12A):1907-1912 (in Chinese with English abstract).
    [4]Clarke EM,Schlingloff H.Model checking.In:Robinson A,Voronkov A,eds.Handbook of Automated Reasoning.Elsevier Science,2001.1635-1790.
    [5]Clarke EM,Kurshan RP.Computer-Aided verification.IEEE Spectrum,1996,33(6):61-67.
    [6]Rajamani SK,Henzinger TA.New directions in refinement checking[Ph.D.Thesis].Berkeley:University of California,1999.
    [7]Kupferman O,Vardi MY.An automata-theoretic approach to modular model checking.ACM Trans.on Programming Languages and Systems,2000,22(1):87-128.
    [8]Berezin S,Ser C,Clarke EM.Compositional reasoning in model checking.LNCS 1536,1998.81-102.
    [9]Henzinger TA,Qadeer S,Rajamani SK,Tasiran S.An assume-guarantee rule for checking simulation.ACM Trans.on Programming Languages and Systems,2002,24(1):51-64.
    [10]Vardi MY.Verification of open systems.In:Ramesh S,Sivakumar G,eds.Proc.of the FSTTCS 1997.Springer-Verlag,1997.250-266.
    [11]Grumberg O,Long DE.Model checking and modular verification.ACM Trans.on Programming Languages and Systems,1994,16(3):843-871.
    [12]Bustan D,Grumberg O.Applicability of fair simulations.In:Katoen JP,Stevens P,eds.Proc.of the Int'l Conf.on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2002).Heidelberg:Springer-Verlag,2002.401-414.
    [13]Long DE.Model checking,abstraction,and compositional verification[Ph.D.Thesis].Pittsburgh:Carnegie Mellon University,1993.
    [14]Alur R,Henzinger TA.Reactive modules.In:Clarke E,ed.Proc.of the 11th Annual Symp.on Logic in Computer Science.IEEE Computer Society Press,1996.207-218.
    [15]McMillan KL.A compositional rule for hardware design refinement.In:Grumberg O,ed.Proc.of the 9th Int'l Conf.on Computer Aided Verification.London:Springer-Verlag,1997.24-35.
    [16]Kurshan RP.Computer-Aided Verification of Coordinating Processes.Princeton:Princeton University Press,1994.
    [17]Stockmeyer LJ,Meyer AR.Word problems requiring exponential time.In:Proc.of the 5th Annual ACM Symp.on Theory of Computing.ACM Press,1973.1-9.
    [18]Gerth R,Peled D,Vardi MY,Wolper P.Simple on-the-fly automatic verification of linear temporal logic.In:Dembinski P,Sredniawa M,eds.Proc.of the 15th IFIP WG6.1 Int'l Symp.on Protocol Specification,Testing and Verification XV.Chapman & Hall,Ltd.,1996.3-18.
    [19]Vardi MY,Wolper P.Reasoning about infinite computations.Information and Computation,1994,115(1):1-37.
    [20]Stark EW.Foundations of a theory of specification for distributed systems.Technical Report,MIT-LCS-TR-342,Massachusetts Institute of Technology,1984.
    [21]Abadi M,Lamport L.Composing specification.ACM Trans.on Programming Languages and Systems (TOPLAS),1993,15(1):73-132.
    [22]Abadi M,Lamport L.Conjoining specifications.ACM Trans.on Programming Languages and Systems (TOPLAS),1995,17(3):507-535.
    [23]Xu Q,Cau A,Collette P.On unifying assumption-commitment style proof rules for concurrency.In:Proc.of the Int'l Conf.on Concurrency Theory.London:Springer-Verlag,1994.267-282.
    [24]Jonsson B,Tsay YK.Assumption/Guarantee specifications in linear-time temporal logic.Theoretical Computer Science,1996,167:47-72.
    [25]Viswanathan M,Viswanathan R.Foundations for circular compositional reasoning.In:Orejas F,Spirakis PG,Leeuwen JV,eds.Proc.of the ICALP 2001.Springer-Verlag,2001.835-847.
    [26]Maier P.A lattice-theoretic framework for circular assume-guarantee reasoning[Ph.D.Thesis].Saarbrücken:Universit(a)t Saarbrücken,2003.
    [27]Amla N,Emerson EA,Namjoshi KS,Trefler RJ.Abstract patterns of compositional reasoning.In:Amadio RM,Lugiez D,eds.Proc.of the 14th Int'l Conf.on CONCUR 2003-Concurrency Theory.Springer-Verlag,2003.423-438.
    [28]Peng H,Tahar S.A survey on compositional verification.Technical Report,Department of Electrical and Computer Engineering,Concordia University,1998.
    [29]Clarke E,Long D,McMillan K.Compositional model checking.In:Parikh R,ed.Proc.of the 4th Annual Symp.on Logic in Computer Science.IEEE Press,1989.353-362.
    [30]Furia CA.A compositional world:A survey of recent works on compositionality in formal methods.Technical Report,2005.22,Dipartimento di Elettronica e Informazione,Politecnico di Milano,2005.
    [31]Alfaro LD,Henzinger TA.Interface automata.In:Gruhn V,ed.Proc.of the 9th Symp.Foundations of Software Engineering.ACM Press,2001.109-120.
    [32]Kupferman O,Piterman N,Vardi M.Extended temporal logic revisited.In:Kim GL,Mogens N,eds.Proc.of the 12th Int'l Conf.on Concurrency Theory.Springer-Verlag,2001.519-535.
    [33]Ghica DR.A games-based foundation for compositional software model checking[Ph.D.Thesis].Kingston:Queen's University,2002.
    [34]Abramsky S,Ghica DR,Murawski AS,Ong CHL.Applying game semantics to compositional software modeling and verifications.In:Kurt J,Andreas P,eds.Proc.of the 10th Int'l Conf.on Tools and Algorithms for the Construction and Analysis of System (TACAS 2004).Springer-Verlag,2004.421-435.
    [3]林惠民,张文辉.模型检测:理论、方法与应用.电子学报,2002,30(12A):1907-1912.
    Related
    Cited by
    Comments
    Comments
    分享到微博
    Submit
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
You are the first2050505Visitors
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