{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,5,6]],"date-time":"2023-05-06T16:40:14Z","timestamp":1683391214966},"reference-count":110,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2006,2,25]],"date-time":"2006-02-25T00:00:00Z","timestamp":1140825600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2006,2,25]],"date-time":"2006-02-25T00:00:00Z","timestamp":1140825600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Innovations Syst Softw Eng"],"published-print":{"date-parts":[[2006,3]]},"DOI":"10.1007\/s11334-006-0021-9","type":"journal-article","created":{"date-parts":[[2006,2,24]],"date-time":"2006-02-24T10:27:27Z","timestamp":1140776847000},"page":"49-64","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":6,"title":["State-rich model checking"],"prefix":"10.1007","volume":"2","author":[{"given":"Leo","family":"Freitas","sequence":"first","affiliation":[]},{"given":"Jim","family":"Woodcock","sequence":"additional","affiliation":[]},{"given":"Ana","family":"Cavalcanti","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2006,2,25]]},"reference":[{"key":"21_CR1","doi-asserted-by":"crossref","unstructured":"Abdallah AE, Jones CB, Sanders JW (eds) (2004) Communicating sequential process: the first 25 years, no. 3525, in Lecture Notes in Computer Science, symposion on the occasion of 25 years of CSP, Springer, London UK, July 2004","DOI":"10.1007\/b136154"},{"key":"21_CR2","doi-asserted-by":"crossref","unstructured":"Abrial J-R (1996) The B book\u2013-assigning programs to meanings. Cambridge University Press, Cambridge","DOI":"10.1017\/CBO9780511624162"},{"key":"21_CR3","doi-asserted-by":"crossref","unstructured":"Alur R, Henzinger T, Mang F, Qadeer S, Rajamani S, Tasinan S (2002) Mocha: Modularity in model checking. Computer Aided Verification, pp. 521\u2013525, 1998.","DOI":"10.1007\/BFb0028774"},{"key":"21_CR4","unstructured":"Amey P (2005) Correctness by construction: better can also be cheaper. Crosstalk J Def Softw Eng Dec: 5\u20138"},{"key":"21_CR5","unstructured":"Atiya D, King S, Woodcock JCP (2003) Ravenscar protected objects: a Circus semantics. Technical Report 356, Department of Computer Science, University of York, York"},{"key":"21_CR6","unstructured":"Austin PD, Welch PH (2000) Java communicating sequential process\u2013-JCSP. http:\/\/www.cs.ukc.ac.uk\/projects\/ofa\/jcsp\/"},{"key":"21_CR7","doi-asserted-by":"crossref","unstructured":"Back R-J, von Wright J (1998) Refinement calculus: A systematic introduction. Graduate text in computer science. Springer, Berlin Heidelberg New York","DOI":"10.1007\/978-1-4612-1674-2_1"},{"key":"21_CR8","doi-asserted-by":"crossref","unstructured":"Ball T, Cook B, Das S, Rajamani SK (2004) Refining approximations in software predicate abstraction. In: Proceedings of 10th international conference on tools and algorithms for the construction and analysis of systems \u2013 TACAS'04, pp. 388\u2013403","DOI":"10.1007\/978-3-540-24730-2_30"},{"key":"21_CR9","unstructured":"Barnes J (2003) High integrity software: the spark approach to safety and security, 2nd edn. Addison\u2013Wesley, Reading"},{"key":"21_CR10","unstructured":"Bensalem S, Ganesh V, Lakhnech Y, Munoz C, Owre S, Rue\u00dfH, Rushby J, Rusu V, Sa\u00efdi H, Shankar N, Singerman E, Tiwari A (2000) An overview of SAL. In: Holloway CM (ed.) LFM 2000: 5th NASA Langley formal methods workshop. NASA Langley Research Center, Hampton, VA, pp. 187\u2013196"},{"key":"21_CR11","doi-asserted-by":"crossref","unstructured":"Biere A, Cimatti A, Clarke EM, Fujita M, Zhu Y (1999) Symbolic model checking using SAT procedures instead of BDDs. In: DAC '99: Proceedings of the 36th ACM\/IEEE conference on design automation, ACM, New York, pp. 317\u2013320","DOI":"10.1145\/309847.309942"},{"issue":"8","key":"21_CR12","doi-asserted-by":"crossref","first-page":"677","DOI":"10.1109\/TC.1986.1676819","volume":"35","author":"RE Bryant","year":"1986","unstructured":"Bryant RE (1986) Graph-based algorithms for boolean function manipulation. IEEE Trans Comput 35(8):677\u2013691","journal-title":"IEEE Trans Comput"},{"key":"21_CR13","doi-asserted-by":"crossref","first-page":"401","DOI":"10.1109\/43.275352","volume":"13","author":"I Burch","year":"1994","unstructured":"Burch I (1994) Symbolic Model Checking for Sequential Circuit Verification. IEEE Trans Comput Aided Des Integr Circ Syst 13:401\u2013424","journal-title":"IEEE Trans Comput Aided Des Integr Circ Syst"},{"key":"21_CR14","unstructured":"Burdy L, Cheon Y, Cok DR, Ernst MD, Kiniry JR, Leavens GT, Rustan K, Leino M, Poll5 E (2003) An overview of JML tools and applications. In: Eighth international workshop on formal methods for industrial critical systems (FMICS), Electronic Notes in Theoretical Computer Science. University of Nijmegen, Elsevier, pp. 73\u201389"},{"key":"21_CR15","doi-asserted-by":"crossref","unstructured":"Butler M, Leuschel M (2005) Combining CSP and B for specification and property verification. In: Fitzgerald J, Hayes IJ, Tarlecki A (eds.) FM 2005: Formal methods, no. 3582, Lecture Notes in Computer Science, Springer, Berlin Heidelberg New York, pp. 221\u2013236","DOI":"10.1007\/11526841_16"},{"key":"21_CR16","unstructured":"Cavada R, Cimatti A, Olivetti E, Pistore M, Roveri M (2005) NuSMV 2.2 user's manual. Carneige Mellon University, Trento, Italy, nusmv.irst.itc.it"},{"key":"21_CR17","doi-asserted-by":"crossref","unstructured":"Chaki S, Clarke EM, Ouaknine J, Sharygina N, Sinha N (2004) State\/event-based software model checking. In: Boiten EA, Derrick J, Smith G (eds.) In: Proceedings of the 4th international conference in integrated formal methods, no. 2999, Lecture Notes in Computer Science, pp. 128\u2013147","DOI":"10.1007\/978-3-540-24756-2_8"},{"key":"21_CR18","unstructured":"Clarke EM, Jha S (1993) Symmetry and induction in model checking. Technical report, Carnegie Mellon University, Pittsburgh"},{"issue":"4","key":"21_CR19","doi-asserted-by":"crossref","first-page":"626","DOI":"10.1145\/242223.242257","volume":"28","author":"EM Clarke","year":"1996","unstructured":"Clarke EM, Wing JM (1996) Formal methods\u2013-state of the art and future directions. ACM Comput Surv 28(4):626\u2013643","journal-title":"ACM Comput Surv"},{"key":"21_CR20","unstructured":"Clarke EM, Grumberg O, Peled D (2000) Model checking. MIT Press, Cambridge"},{"issue":"1","key":"21_CR21","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1007\/BF01211314","volume":"5","author":"R Cleaveland","year":"1993","unstructured":"Cleaveland R, Hennessy M (1993) Testing equivalence as a bisimulation equivalence. Formal Aspects Comput J 5(1):1\u201320","journal-title":"Formal Aspects Comput J"},{"key":"21_CR22","unstructured":"Cleaveland R, Iyer P, Yankelevich D (1993) Optimality in abstractions of model checking. Technical report, North Carolina State University, US and University of Buenos Aires, Argentina"},{"key":"21_CR23","doi-asserted-by":"crossref","unstructured":"Cook B, Podelski A, Rybalchenko A (2005) Abstraction refinement for termination. In: Proceedings of international static analysis symposium \u2013 SAS'05, London","DOI":"10.1007\/11547662_8"},{"issue":"4","key":"21_CR24","doi-asserted-by":"crossref","first-page":"511","DOI":"10.1093\/logcom\/2.4.511","volume":"2","author":"P Cousot","year":"1992","unstructured":"Cousot P, Cousot R (1992) Abstract interpretation framworks. J Logic Comput 2(4):511\u2013547","journal-title":"J Logic Comput"},{"key":"21_CR25","doi-asserted-by":"crossref","unstructured":"Deharbe D, Shankar S, Clarke EM Jr (1998) Model checking VHDL with CV. In: Formal methods in circuit automation design (FMCAD'98), Lecture Notes in Computer Science, vol. 1522. Springer, Berlin Heidelberg New York, pp. 508\u2013513","DOI":"10.1007\/3-540-49519-3_33"},{"key":"21_CR26","unstructured":"Detlefs D, Rustan K, Leino M, Nelson G, Saxe JB (1998) Extended static checking. Technical Report 159, COMPAQ Systems Research Center (SRC), http:\/\/www.research.digital.com\/SRC\/"},{"key":"21_CR27","unstructured":"Dovier A, Piazza C, Policriti A (2000) A fast bisimulation algorithm. Technical report, University di Verona and University Udine, November 2000, UDM\/14\/00\/RR"},{"issue":"1\u20132","key":"21_CR28","first-page":"99","volume":"29","author":"W Elseaidy","year":"1994","unstructured":"Elseaidy W (ed.) (1994) Modeling and verifying active structural control systems. Sci Comput Program 29(1\u20132):99\u2013122","journal-title":"Sci Comput Program"},{"key":"21_CR29","unstructured":"Farias AC (2003) Efficient and mechanised analysis of infinite CSP-Z processes. Master's thesis, Universidade Federal de Pernambuco, Pernambuco"},{"key":"21_CR30","unstructured":"Fischer C (2000) Combination and implementation of process and data: From CSP-OZ to Java. PhD thesis, University of Oldenburg, Oldenburg"},{"key":"21_CR31","unstructured":"Formal Systems (Europe) Ltd. (2000) ProBE user's manual version 1.28"},{"key":"21_CR32","unstructured":"Freitas L (2004) Predicate transition system\u2013-automata theory. Appendix A.3 in [34] (CD-ROM)"},{"key":"21_CR33","unstructured":"Freitas L (2005) Model checking Circus. PhD thesis, Univeristy of York, York"},{"key":"21_CR34","doi-asserted-by":"crossref","unstructured":"Freitas L, Cavalcanti A, Sampaio A (2002) JACK\u2013-a framework for process algebra implementation in Java. In: Proceedings of XVIII Simposio Brasileiro de Engenharia de Software in Gramado, October 2002, pp. 98\u2013113","DOI":"10.5753\/sbes.2002.23941"},{"key":"21_CR35","unstructured":"Goldsmith M (2000) FDR2 user's manual version 2.67. Formal Systems (Europe) Ltd, Oxford"},{"key":"21_CR36","unstructured":"Goldsmith M (2001) Overview of FDR in [94], chap. 4. Addison\u2013Wesley, Reading, pp. 125\u2013140"},{"issue":"1","key":"21_CR37","doi-asserted-by":"crossref","first-page":"18","DOI":"10.1109\/52.976937","volume":"19","author":"A Hall","year":"2002","unstructured":"Hall A, Chapman R (2002) Correctness by construction: developing a commercial secure system. IEEE Softw J 19(1):18\u201325","journal-title":"IEEE Softw J"},{"key":"21_CR38","doi-asserted-by":"crossref","unstructured":"Har'el Z, Kurshan RP (1990) Software for analytical development of communications protocols. AT&T Tech J 69(1):45\u201359","DOI":"10.1002\/j.1538-7305.1990.tb00102.x"},{"issue":"10","key":"21_CR39","doi-asserted-by":"crossref","first-page":"576","DOI":"10.1145\/363235.363259","volume":"12","author":"CAR Hoare","year":"1969","unstructured":"Hoare CAR (1969) An axiomatic basis for computer programming. Commun ACM 12(10):576\u2013583","journal-title":"Commun ACM"},{"key":"21_CR40","unstructured":"Hoare CAR, Jifeng H (1998) Unifying Theories of Programming. International series in computer science. Prentice-Hall, Englewood Cliffs"},{"issue":"5","key":"21_CR41","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1109\/32.588521","volume":"23","author":"GJ Holzmann","year":"1997","unstructured":"Holzmann GJ (1997) The Model-Checker SPIN. IEEE Trans Softw Eng 23(5):1\u201317","journal-title":"IEEE Trans Softw Eng"},{"key":"21_CR42","doi-asserted-by":"crossref","unstructured":"Hopcroft J, Motwani R, Ullman JD (2001) Introduction to automata theory, languages, and computation, 2nd edn. Addison\u2013Wesley, Reading","DOI":"10.1145\/568438.568455"},{"key":"21_CR43","unstructured":"The ICS Group (2005) ICS Manual (Version 2.0). SRI International, Computer Science Laboratory, SRI International 333 Ravenswood Avenue, Menlo Park, CA 94025, USA"},{"key":"21_CR44","doi-asserted-by":"crossref","unstructured":"Jackson D, Schechter I, Shlyakhter I (2000) Alcoa: the alloy constraint analyzer. In: Proceedings of the 22nd international conference on software engineering, June 2000, pp. 730\u2013733","DOI":"10.1145\/337180.337616"},{"key":"21_CR45","unstructured":"Jones G, Goldsmith M (1998) Programming in occam 2. International series in computer science, 2nd edn. Prentice-Hall, Englewood Cliffs"},{"key":"21_CR46","doi-asserted-by":"crossref","unstructured":"Kang H-J, Park I-C (2003) SAT-based unbounded symbolic model checking. In: Proceedings of the 40th design automation conference (DAC'03), IEEE, pp. 840\u2013843","DOI":"10.1145\/775832.776043"},{"key":"21_CR47","unstructured":"Kokkarinen I (1998) A veridication-oriented theory of data in labelled transition systems. PhD thesis, Tampere University, Finland"},{"key":"21_CR48","doi-asserted-by":"crossref","first-page":"333","DOI":"10.1016\/0304-3975(82)90125-6","volume":"27","author":"D Kozen","year":"1998","unstructured":"Kozen D (1998) Results on the propositional \u03bc-calculus. Theor Comput Sci 27:333\u2013354","journal-title":"Theor Comput Sci"},{"key":"21_CR49","doi-asserted-by":"crossref","unstructured":"Lahriri SK, Ball T, Cook B (2005) Predicate abstraction via symbolic decision procedures. Technical Report MSR-TR-2005-53, Microsoft Research","DOI":"10.1007\/11513988_5"},{"key":"21_CR50","unstructured":"Lazi\u0107 RS (1999) A semantic study of data independence with applications to model checking. PhD thesis, Programming Research Group, Oxford University, Oxford"},{"key":"21_CR51","unstructured":"Lemma-One (2003) ProofPower Tutorial"},{"key":"21_CR52","doi-asserted-by":"crossref","unstructured":"Leuschel MA, Massart T, Currie A (2001) How to make FDR spin: LTL model checking of CSP by refinement. In: Oliveira JN, Zave P (eds.) Formal methods Europe 2001, vol. 2021. Springer, Berlin Heidelberg New York, pp. 99\u2013118","DOI":"10.1007\/3-540-45251-6_6"},{"key":"21_CR53","unstructured":"Leuschel LA, Butler M, Lo Presti S (2005) ProB User Manual version 1.1.4. Declarative systems and software engineering, University of Southampton, and Softwaretechnik und Programmiersprachen, University of D\u00fcusseldorf, Germany"},{"key":"21_CR54","unstructured":"Lowe G (1996) A hierarchy of authentication specifications. Technical report, University of Leicester, Leicester"},{"key":"21_CR55","unstructured":"Lowe G (1997) CASPER user manual. Oxford University, Oxford"},{"key":"21_CR56","unstructured":"Lowe G (2002) Simplifying transformations\u2013-the CyberCash security protocol in [94], chap. 8. Addison Wesley, Reading, pp. 201\u2013220"},{"key":"21_CR57","doi-asserted-by":"crossref","unstructured":"Lowe G, Roscoe B (1997) Using CSP to detect errors in the TMN protocol. Technical report, Oxford University, Oxford","DOI":"10.1109\/32.637148"},{"key":"21_CR58","doi-asserted-by":"crossref","unstructured":"Malik P, Utting M (2005) CZT: A framework for Z tools. In: Treharne H, King S, Henson M, Schneider S (eds.) ZB 2005: Formal specification and development in Z and B: 4th international conference of B and Z users, Guildford, UK, Springer, Berlin Heidelberg New York, pp. 13\u201315","DOI":"10.1007\/11415787_5"},{"key":"21_CR59","doi-asserted-by":"crossref","unstructured":"Manna Z, Pnueli A (1992) The temporal logic of reactive and concurrent systems\u2013-specification, vol. 1. Springer, Berlin Heidelberg New York","DOI":"10.1007\/978-1-4612-0931-7"},{"key":"21_CR60","unstructured":"Manna Z, Pnueli A (1995) The temporal logic of reactive and concurrent systems\u2013-safety, vol. 2. Springer, Berlin Heidelberg New York"},{"key":"21_CR61","unstructured":"Martin JMR (1996) The design and construction of deadlock-free concurrent systems. PhD thesis, University of Buckingham, Buckingham"},{"key":"21_CR62","unstructured":"Martin JMR, Huddart Y (2000) Parallel algorithms for deadlock and livelock analysis of concurrent systems. Communicating Process Architectures IOS Press."},{"key":"21_CR63","doi-asserted-by":"crossref","unstructured":"McMillan KL (1993) Symbolic model checking. Kluwer, Dordrecht","DOI":"10.1007\/978-1-4615-3190-6"},{"key":"21_CR64","unstructured":"Microsoft Research (2004) SLAM: A static driver verifier. research.microsoft.com\/slam\/"},{"key":"21_CR65","unstructured":"Milner R (1990) Communication and concurrency. International series in Computer lence. Prentice-Hall, Englewood Cliffs"},{"issue":"4","key":"21_CR66","doi-asserted-by":"crossref","first-page":"417","DOI":"10.1109\/TSE.1981.230844","volume":"7","author":"J Misra","year":"1990","unstructured":"Misra J, Chandy KM (1990) Proofs of networks of processes. IEEE Trans Softw Eng SE 7(4):417\u2013426","journal-title":"IEEE Trans Softw Eng SE"},{"key":"21_CR67","unstructured":"Morgan C (1994) Programming from specifications. Prentice-Hall, Englewood Cliffs"},{"key":"21_CR68","unstructured":"Mota A (1997) Formalization and analysis of the SACI-1 micro satellite in CSP-Z. Master's thesis, Universidade Federal de Pernambuco, Pernambuco (in Portuguese)"},{"key":"21_CR69","unstructured":"Mota A (2001) Model cecking CSP-Z: Techniques to overcome state explosion. PhD thesis, Universidade Federal de Pernambuco, Pernambuco"},{"key":"21_CR70","unstructured":"Mota A, Sampaio A (2001) Model checking CSP-Z. Science of computer programming, vol. 4. Elsevier, Amsterdam"},{"key":"21_CR71","doi-asserted-by":"crossref","unstructured":"de Moura L, Rue\u00df H, Sorea M (2002) Lazy theorem proving for bounded model checking over infinite domains. In: Proceedings of the 18th conference on automated deduction (CADE), Lecture Notes in Computer Science, Copenhagen, Denmark, 27\u201330 July, Springer, Berlin Heidelberg New York","DOI":"10.1007\/3-540-45620-1_35"},{"key":"21_CR72","doi-asserted-by":"crossref","unstructured":"de Moura L, Rue\u00df H, Sorea M (2003) Bounded model checking and induction: From refutation to verification. In: Voronkov A (ed.) Computer-aided verification, CAV 2003, Lecture Notes in Computer Science, vol. 2725. Springer, Berlin Heidelberg New York pp. 14\u201326","DOI":"10.1007\/978-3-540-45069-6_2"},{"key":"21_CR73","doi-asserted-by":"crossref","unstructured":"de Moura L, Owre S, Rue\u00df H, Rushby J, Shankar N, Sorea M, Tiwari A (2004) SAL 2. In: Proceedings of the 16th international conference on computer aided verification (CAV), Lecture Notes in Computer Science, Boston, July 2004, Springer, Berlin Heidelberg New York","DOI":"10.1007\/978-3-540-27813-9_45"},{"key":"21_CR74","unstructured":"Oliveira M (2006) Formal derivation of state-rich reactive programs using Circus. PhD thesis, University of York, York"},{"key":"21_CR75","doi-asserted-by":"crossref","unstructured":"Oliveira M, Cavalcanti A, Woodcock J (2005) Unifying theories in ProofPowerZ Draft, Univeristy of York, York","DOI":"10.1007\/11768173_8"},{"issue":"6","key":"21_CR76","doi-asserted-by":"crossref","first-page":"973","DOI":"10.1137\/0216062","volume":"16","author":"R Paige","year":"1987","unstructured":"Paige R, Tarjan R (1987) Three partition refinement algorithms. SIAM J Comput 16(6):973\u2013989","journal-title":"SIAM J Comput"},{"key":"21_CR77","doi-asserted-by":"crossref","unstructured":"Paranhos D, Cirne W, Brasileiro F (2003) Trading cycles for information: Using replication to schedule bag-of-tasks applications on computational grids. In: Proceedings of the Euro-Par 2003: International conference on parallel and distributed computing, August 2003, pp. 169\u2013180","DOI":"10.1007\/978-3-540-45209-6_26"},{"key":"21_CR78","unstructured":"Parashkevov AN, Yantchev J (1996) ARC\u2013-A tool for efficient refinement and equivalence checking for CSP. In: IEEE 2nd international conference on algorithms and architectures for parallel processing ICA3PP, pp. 68\u201375"},{"key":"21_CR79","unstructured":"Parashkevov AN, Yantchev J (1996) ARC\u2013-A verification tool for concurrent systems. In: Proceedings of the 3rd Australasian parallel and real-time conference. Brisbane, Australia"},{"key":"21_CR80","doi-asserted-by":"crossref","unstructured":"Peled D (1994) Combining partial order reductions with on-the-fly model checking. In: CAV '94: Proceedings of the 6th international conference on computer aided verification. London, UK, Springer, Berlin Heidelberg New York","DOI":"10.1007\/3-540-58179-0_69"},{"key":"21_CR81","doi-asserted-by":"crossref","unstructured":"Pnueli A (1984) In transition for global to modular temporal reasoning about programs. In: Apt KR (ed.) Logics and models of concurrent systems, NATO ASI. Springer, Berlin Heidelberg New York","DOI":"10.1007\/978-3-642-82453-1_5"},{"key":"21_CR82","doi-asserted-by":"crossref","unstructured":"Poll E, van den Berg J, Jacobs B (2000) Specification of the JavaCard API in JML, chap. 3. pp 135\u2013154. Kluwer, Dordrecht. Also Department of Computer Science, University of Nijmegen. CSI report CSI-R0005","DOI":"10.1007\/978-0-387-35528-3_8"},{"issue":"1","key":"21_CR83","doi-asserted-by":"crossref","first-page":"82","DOI":"10.1145\/248621.248624","volume":"29","author":"F Pong","year":"1997","unstructured":"Pong F, Dubois M (1997) Verification techniques for cache coherence protocols. ACM Comput Surv 29(1) 82\u2013126","journal-title":"ACM Comput Surv"},{"key":"21_CR84","doi-asserted-by":"crossref","unstructured":"Rajasekaran S, Lee I (1998) Parallel algorithms for relational coarsest partition problems. In: Proceedings of the IEEE transactions on parallel and distributed systems, vol 9(7). IEEE CS, pp. 687\u2013699[Query17]","DOI":"10.1109\/71.707548"},{"key":"21_CR85","unstructured":"Roscoe AW (ed.) (1994) A classical mind: Essays in honour of C. A. R. Hoare. International series in computer science. Prentice-Hall, Englewood Cliffs"},{"key":"21_CR86","unstructured":"Roscoe AW (1994) Model checking CSP in [86], chap. 21. Prentice-Hall, Englewood Cliffs, pp. 353\u2013378"},{"key":"21_CR87","unstructured":"Roscoe AW (1997) The theory and practice of concurrency. International series in computer science. Prentice-Hall, Englewood Cliffs"},{"key":"21_CR88","unstructured":"Roscoe AW, MacCarthy H (1994) Verifying a replicated database: A case study in model checking CSP. Technical report, Oxford University, Oxford"},{"key":"21_CR89","doi-asserted-by":"crossref","unstructured":"Roscoe AW, Gardiner PHB, Goldsmith MH, Hulance JR, Jackson DM, Scattergood JB (1995) Hierarchical compression for model checking CSP or how to check 1020 dining philosophers for deadlock. First TACAS in Lecture Notes in Computer Science, vol. 1019(1)","DOI":"10.1007\/3-540-60630-0_7"},{"key":"21_CR90","unstructured":"Rushby J (1995) Model checking and other ways of automating formal methods. Model checking for concurrent programs software, quality week\u2013-San Francisco, Position Paper\u2013\u2013SRI International"},{"key":"21_CR91","unstructured":"Rushby J (1997) Specification, proof checking, and model checking for protocols and distributed systems with PVS. Formal description techniques and protocol specification, testing and verification (FORTE\/PSTV)\u2013-Osaka, Japan; SRI international\u2013-paper and tutorial slides, pp. 9\u201312"},{"key":"21_CR92","doi-asserted-by":"crossref","unstructured":"Rushby J (1999) Mechanised formal methods: Where next? In: The World congress on formal methods\u2013-Toulouse France, no. 1708, Lecture Notes in Computer Science, Springer, Berlin Heidelberg New York. pp. 48\u201351, invited paper; SRI international\u2013-paper and tutorial slides","DOI":"10.1007\/3-540-48119-2_3"},{"key":"21_CR93","doi-asserted-by":"crossref","unstructured":"Rushby J (2000) From refutation to verification. Formal description techniques and protocol specification, testing and verification (FORTE XIII\/PSTV XX)\u2013-Pisa, Italy, pp. 369\u2013374","DOI":"10.1007\/978-0-387-35533-7_23"},{"key":"21_CR94","unstructured":"Ryan P, Schneider S, Roscoe B, Goldsmith M, Lowe G (2001) Modelling and analysis of security protocols. Addison-Wesley, Reading"},{"key":"21_CR95","unstructured":"Saaltink M (1992) Z\/Eves 2.0 user's guide. ORA Canada TR-99-5493-06a"},{"key":"21_CR96","unstructured":"Scattergood JB (1992) A parser for CSP. Technical report, Oxford University, Oxford"},{"key":"21_CR97","unstructured":"Schneider S (1997) Verifying authentication protocols with CSP. Technical report, Royal Holloway, University of London, London"},{"key":"21_CR98","unstructured":"Schneider S (1998) Security properties and CSP. Technical report, Royal Holloway, University of London, London"},{"key":"21_CR99","unstructured":"Shankar N (2002) Mechanised verification methodologies. In: Summer school in specification, verification, and refinement, Turku, Finland"},{"key":"21_CR100","unstructured":"Shankar N, Sorea M (2004) Counterexample-driven model checking. CSL technical report SRI-CSL-03-04, SRI International"},{"key":"21_CR101","unstructured":"Spivey JM (1998) The Z notation: a reference manual. Prentice-Hall, Englewood Cliffs"},{"key":"21_CR102","doi-asserted-by":"crossref","unstructured":"Valmari A (1990) A stubborn attack on state explosion in [18], chap. 2. No. 531, Lecture Notes in Computer Science. Springer, Berlin Heidelberg New York, pp. 156\u2013165","DOI":"10.1007\/BFb0023729"},{"key":"21_CR103","unstructured":"Valmari A (2005) What does theory say about the possibilities of improving efficiency. UK Model Checking Days, University of York, York, http:\/\/www.cs.york.ac.uk\/~luettgen\/ukmcdays"},{"issue":"3","key":"21_CR104","doi-asserted-by":"crossref","first-page":"147","DOI":"10.1007\/s001650070026","volume":"12","author":"H Wehrheim","year":"2000","unstructured":"Wehrheim H (2000) Data abstraction techniques in the validation of csp-oz specifications. Formal Aspects Comput J 12(3):147\u2013164","journal-title":"Formal Aspects Comput J"},{"key":"21_CR105","doi-asserted-by":"crossref","unstructured":"Williams PF, Biere A, Clarke EM, Gupta A (2000) Combining decision diagrams and SAT procedures for efficient symbolic model checking. In: CAV '00: Proceedings of the 12th international conference on computer aided verification, London, UK, Springer, Berlin Heidelberg New York, pp. 124\u2013138","DOI":"10.1007\/10722167_13"},{"key":"21_CR106","unstructured":"Woodcock J (2003) UK grand challenge in computer science: dependable systems evolution. http:\/\/www.nesc.ac.uk"},{"key":"21_CR107","unstructured":"Woodcock J, Davies J (1996) Using Z: Specification, refinement, and proof. International series in computer science. Prentice-Hall, Englewood Cliffs"},{"key":"21_CR108","unstructured":"Woodcock JCP, Cavalcanti ALC (2001) The steam boiler in a unified theory of Z and CSP. In: Proceedings of 8th Asia\u2013Pacific software engineering conference (APSEC01), IEEE Computer Society, pp. 291\u2013298"},{"key":"21_CR109","doi-asserted-by":"crossref","unstructured":"Woodcock J, Cavalcanti A (2002) Circus \u2013-a concurrent language for refinement. Technical report, University of Kent, Canterbury","DOI":"10.14236\/ewic\/IWFM2001.7"},{"key":"21_CR110","unstructured":"Z Standard (2000) Formal specification, Z notation, syntax, type and semantics\u2013-consensus working draft 2.6. Technical Report JTC1.22.45, BSI panel IST\/5\/-\/19\/2 (Z notation) and ISO panel JTC1\/SC22\/WG19 (Rapporteur Group for Z),http:\/\/www.cs.york.ac.uk\/~ian\/zstan\/"}],"container-title":["Innovations in Systems and Software Engineering"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s11334-006-0021-9.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s11334-006-0021-9\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s11334-006-0021-9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s11334-006-0021-9.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,5,6]],"date-time":"2023-05-06T16:00:40Z","timestamp":1683388840000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s11334-006-0021-9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006,2,25]]},"references-count":110,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2006,3]]}},"alternative-id":["21"],"URL":"https:\/\/doi.org\/10.1007\/s11334-006-0021-9","relation":{},"ISSN":["1614-5046","1614-5054"],"issn-type":[{"value":"1614-5046","type":"print"},{"value":"1614-5054","type":"electronic"}],"subject":[],"published":{"date-parts":[[2006,2,25]]},"assertion":[{"value":"21 October 2005","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"8 December 2005","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"25 February 2006","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}