Model checking of state-rich formalism by linking to \(CSP\,\Vert \,B\)

详细信息    查看全文

• 作者：Kangfeng Ye…
• 关键词：\(CSP \parallel B\) ; CSP ; Z ; B ; ProB ; Model checking ; Buffer
• 刊名：International Journal on Software Tools for Technology Transfer
• 出版年：2017
• 出版时间：February 2017
• 年：2017
• 卷：19
• 期：1
• 页码：73-96
• 全文大小：
• 刊物类别：Computer Science
• 刊物主题：Software Engineering; Software Engineering/Programming and Operating Systems; Theory of Computation;
• 出版者：Springer Berlin Heidelberg
• ISSN：1433-2787
• 卷排序：19

文摘

Since state-rich formalism is a combination of Z, CSP, refinement calculus and Dijkstra’s guarded commands, its model checking is intrinsically more complicated and difficult than that of individual state-based languages or process algebras. Current solutions translate executable constructs of programs to Java with JCSP, or translate them to CSP processes. Data aspects of programs are expressed in the Java programming language or as CSP processes. Both of them have disadvantages. This work presents a new approach to model-checking by linking it to \(CSP \parallel B\); then we utilise ProB to model-check and animate the \(CSP \parallel B\) program. The most significant advantage of this approach is the direct mapping of the state part in to Z and finally to B, which maintains the high-level abstraction of data specification. In addition, introduction of deadlock, invariant violation checking, LTL formula checking and animation is another key advantage. We present our approach, a link definition for a subset of constructs, as well as a popular case study (reactive buffer) to show the practical usability of our work. We conclude with a discussion of related work, advantages and potential limitations of our approach and future work.Keywords\(CSP \parallel B\)CSPZBProBModel checkingBufferReferences1.FDR2: a refinement checker for establishing properties of models expressed in CSP. www.fsel.com/software.html 2.SICStus prolog manual (arithmetic expressions). https://sicstus.sics.se/sicstus/docs/latest4/html/sicstus.html/ref_002dari_002daex.html#ref_002dari_002daex 3.The ProB animator and model checker. http://www.stups.uni-duesseldorf.de/ProB/index.php5/Main_Page 4.ISO/IEC: Information technology-Z formal specification notation-syntax, type system and semantics (2002). http://standards.iso.org/ittf/PubliclyAvailableStandards/c021573_ISO_IEC_13568_2002(E).zip 5.Abrial, J.R.: The B-book: Assigning Programs to Meanings. Cambridge University Press, Cambridge (2005)MATHGoogle Scholar6.Abrial, J.R.: Modeling in Event-B: System and Software Engineering. Cambridge University Press, Cambridge (2010)CrossRefMATHGoogle Scholar7.Beg, A., Butterfield, A.: Linking a state-rich process algebra to a state-free algebra to verify software/hardware implementation. In: Proceedings of the 8th International Conference on Frontiers of Information Technology (FIT ’10), pp. 47:1–47:5. ACM, New York (2010)8.Bergstra, J.A., Klop, J.W.: Process algebra for synchronous communication. Inf. Control 60(1–3), 109–137 (1984)MathSciNetCrossRefMATHGoogle Scholar9.Butler, M., Leuschel, M.: Combining CSP and B for specification and property verification. In: Fitzgerald, J., Hayes, I.J., Tarlecki, A. (eds.) FM 2005: Formal Methods. Lecture Notes in Computer Science, vol. 3582, pp. 221–236. Springer, Berlin, Heidelberg (2005)CrossRefGoogle Scholar10.Carlsson, M.: Sicstus PROLOG user’s manual 4. Swedish Institute of Computer Science (2015). ISBN: 9783735737441. https://sicstus.sics.se/sicstus/docs/latest4/pdf/sicstus.pdf 11.Carrington, D.A., Duke, D.J., Duke, R., King, P., Rose, G.A., Smith, G.: Object-Z: an object-oriented extension to Z. In: Formal Description Techniques for Distributed Systems and Communication Protocols (FORTE ’89), pp. 281–296. North-Holland Publishing Co., Amsterdam (1990)12.Cavalcanti, A., Sampaio, A., Woodcock, J.: A refinement strategy for Circus. Form. Asp. Comput. 15(2–3), 146–181 (2003)CrossRefMATHGoogle Scholar13.Cavalcanti, A., Woodcock, J.: A tutorial introduction to CSP in unifying theories of programming. In: Cavalcanti, A., Sampaio, A., Woodcock, J. (eds.) Refinement Techniques in Software Engineering. Lecture Notes in Computer Science, vol. 3167, pp. 220–268. Springer, Berlin, Heidelberg (2006)CrossRefGoogle Scholar14.Clarke Jr, E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, Cambridge (1999)Google Scholar15.Clearsy: B language reference manual (version 1.8.6). http://www.atelierb.eu/ressources/manrefb1.8.6.uk.pdf 16.Dijkstra, E.W.: A Discipline of Programming. Prentice-Hall, Englewood Cliffs (1976)MATHGoogle Scholar17.Eclipse: Eclipse public license–v 1.0. http://www.eclipse.org/org/documents/epl-v10.html 18.Fischer, C.: CSP-OZ: a combination of object-Z and CSP (1997)19.Fischer, C.: How to combine Z with process algebra. In: ZUM, pp. 5-23 (1998)20.Formal systems (Europe) Ltd: FDR2 user manual, fdr 2.94 edn (2012)21.Freitas, L.: Model checking Circus. Ph.D. thesis (2005)22.Freitas, A., Cavalcanti, A.: Automatic translation from Circus to Java. In: Misra, J., Nipkow, T., Sekerinski, E. (eds.) FM 2006: Formal Methods. Lecture Notes in Computer Science, vol. 4085, pp. 115–130. Springer, Berlin, Heidelberg (2006)CrossRefGoogle Scholar23.Galloway, A., Stoddart, B.: An operational semantics for ZCCS. In: Proceedings of the 1st International Conference on Formal Engineering Methods (ICFEM ’97). IEEE Computer Society, Washington, DC (1997). ISBN: 0-8186-8002-424.Hoare, C., He, J.: Unifying Theories of Programming, vol. 14. Prentice Hall, Englewood Cliffs (1998)25.Hoare, C.A.R.: Communicating Sequential Processes. Prentice-Hall, Englewood Cliffs (1985)MATHGoogle Scholar26.Jones, C.B.: Systematic Software Development using VDM, 2nd edn. Prentice Hall, Englewood Cliffs. Prentice Hall International Series in Computer Science (1991)27.Lamport, L.: Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers. Addison-Wesley, Boston (2002)28.Lazic, R.: A semantic study of data independence with application to model checking. Ph.D. thesis (1999). http://www.dcs.warwick.ac.uk/~lazic/thes_corr.ps.gz 29.Leijen, D.: Division and modulus for computer scientists (2001). http://research.microsoft.com/pubs/151917/divmodnote.pdf 30.Leuschel, M., Butler, M.J.: Automatic refinement checking for B. In: ICFEM, pp. 345-359 (2005)31.Marcel Oliveira Augusto Sampaio, P.A.R.R.A.C.J.W.: Compositional analysis and design of CML models. COMPASS deliverable D24.1 (2013)32.Milner, R.: A Calculus of Communicating Systems. Lecture Notes in Computer Science, vol. 92. Springer, Berlin (1980)33.Morgan, C.C.: Programming from Specifications. Prentice Hall International Series in Computer Science 2nd edn. Prentice Hall, Englewood Cliffs (1994)34.Mota, A., Sampaio, A.: Model-Checking CSP-Z. In: FASE, pp. 205–220 (1998)35.Nogueira, S., Sampaio, A., Mota, A.: Test generation from state based use case models. Form. Asp. Comput. 1-50 (2012). doi:10.1007/s00165-012-0258-z 36.Oliveira, M.V.: Formal derivation of state-rich reactive programs using Circus. Ph.D. thesis, University of York (2005)37.Oliveira, M., Cavalcanti, A., Woodcock, J.: Formal development of industrial-scale systems in Circus. ISSE 1(2), 125–146 (2005)Google Scholar38.Oliveira, M., Cavalcanti, A., Woodcock, J.: A denotational semantics for Circus. Electr. Notes Theor. Comput. Sci. 187, 107–123 (2007)CrossRefGoogle Scholar39.Oliveira, M., Cavalcanti, A., Woodcock, J.: A UTP semantics for Circus. Form. Asp. Comput. 21(1–2), 3–32 (2009)CrossRefMATHGoogle Scholar40.Oliveira, M., Sampaio, A., Conserva Filho, M.: Model-checking Circus state-rich specifications. In: E. Albert, E. Sekerinski (eds.) Integrated Formal Methods, Lecture Notes in Computer Science, pp. 39-54. Springer International Publishing, Berlin (2014). doi:10.1007/978-3-319-10181-1_3 41.Plagge, D., Leuschel, M.: Validating Z specifications using the ProB animator and model checker. In: J. Davies, J. Gibbons (eds.) Integrated Formal Methods, Lecture Notes in Computer Science, vol. 4591, pp. 480-500. Springer, Berlin (2007). doi:10.1007/978-3-540-73210-5_25 42.Roscoe, A.: Understanding Concurrent Systems, 1st edn. Springer, New York (2010)CrossRefMATHGoogle Scholar43.Roscoe, A.W., Hoare, C.A.R., Bird, R.: The Theory and Practice of Concurrency. Prentice Hall PTR, Upper Saddle River, NJ, USA (1997)Google Scholar44.Roscoe, A.W., Woodcock, J., Wulf, L.: Non-interference through determinism. J. Comput. Secur. 4(1), 27–54 (1996)CrossRefGoogle Scholar45.Scattergood, B.: The semantics and implementation of machine-readable CSP. Ph.D. thesis, University of Oxford (1998)46.Schneider, S., Treharne, H.: CSP theorems for communicating B machines. Form. Asp. Comput. 17(4), 390–422 (2005)CrossRefMATHGoogle Scholar47.Spivey, J.M.: Z Notation: A Reference Manual: Prentice Hall International Series in Computer Science, 2nd edn. Prentice Hall, Englewood Cliffs (1992)48.Welch, P.H.: Process oriented design for Java: concurrency for all. In: PDPTA, vol. 1, pp. 51–57. CSREA Press (2000)49.Woodcock, J., Cavalcanti, A.: The semantics of Circus. In: Bert, D., Bowen, J.P., Henson, M.C., Robinson, K. (eds.) ZB 2002: Formal Specification and Development in Z and B. Lecture Notes in Computer Science, vol. 2272, pp. 184–203. Springer, Berlin, Heidelberg (2002) 50.Woodcock, J., Cavalcanti, A.: A tutorial introduction to designs in unifying theories of programming. In: Boiten, E.A., Derrick, J., Smith, G. (eds.) Integrated Formal Methods. Lecture Notes in Computer Science, vol. 2999, pp. 40–66. Springer, Berlin, Heidelberg (2004)CrossRefGoogle Scholar51.Woodcock, J., Cavalcanti, A., Freitas, L.: Operational semantics for model checking Circus. In: Fitzgerald, J., Hayes, I.J., Tarlecki, A. (eds.) FM 2005: Formal Methods. Lecture Notes in Computer Science, vol. 3582, pp. 237–252. Springer, Berlin, Heidelberg (2005)CrossRefGoogle Scholar52.Woodcock, J., Cavalcanti, A., Gaudel, M.C., Freitas, L.: Operational semantics for Circus. Formal aspects of computing (2007). https://www.cs.york.ac.uk/ftpdir/pub/leo/utp/journal-pub/circus-operational-semantics.pdf Copyright information© Springer-Verlag Berlin Heidelberg 2015Authors and AffiliationsKangfeng Ye1Email authorJim Woodcock11.Department of Computer ScienceUniversity of YorkYorkUK About this article CrossMark Publisher Name Springer Berlin Heidelberg Print ISSN 1433-2779 Online ISSN 1433-2787 About this journal Reprints and Permissions Article actions .buybox { margin: 16px 0 0; position: relative; } .buybox { font-family: Source Sans Pro, Helvetica, Arial, sans-serif; font-size: 14px; font-size: .875rem; } .buybox { zoom: 1; } .buybox:after, .buybox:before { content: ''; display: table; } .buybox:after { clear: both; } /*---------------------------------*/ .buybox .buybox__header { border: 1px solid #b3b3b3; border-bottom: 0; padding: 8px 12px; position: relative; background-color: #f2f2f2; } .buybox__header .buybox__login { font-family: Source Sans Pro, Helvetica, Arial, sans-serif; font-size: 14px; font-size: .875rem; letter-spacing: .017em; display: inline-block; line-height: 1.2; padding: 0; } .buybox__header .buybox__login:before { position: absolute; top: 50%; -webkit-transform: perspective(1px) translateY(-50%); transform: perspective(1px) translateY(-50%); content: '\A'; width: 34px; height: 34px; left: 10px; } /*---------------------------------*/ .buybox .buybox__body { padding: 0; padding-bottom: 16px; position: relative; text-align: center; background-color: #fcfcfc; border: 1px solid #b3b3b3; } .buybox__body .buybox__section { padding: 16px 12px 0 12px; text-align: left; } .buybox__section .buybox__buttons { text-align: center; width: 100%; } /********** mycopy buybox specific **********/ .buybox.mycopy__buybox .buybox__section .buybox__buttons { border-top: 0; padding-top: 0; } /******/ .buybox__section:nth-child(2) .buybox__buttons { border-top: 1px solid #b3b3b3; padding-top: 20px; } .buybox__buttons .buybox__buy-button { display: inline-block; text-align: center; margin-bottom: 5px; padding: 6px 12px; } .buybox__buttons .buybox__price { white-space: nowrap; text-align: center; font-size: larger; padding-top: 6px; } .buybox__section .buybox__meta { letter-spacing: 0; padding-top: 12px; } .buybox__section .buybox__meta:only-of-type { padding-top: 0; position: relative; bottom: 6px; } /********** mycopy buybox specific **********/ .buybox.mycopy__buybox .buybox__section .buybox__meta { margin-top: 0; margin-bottom: 0; } /******/ .buybox__meta .buybox__product-title { display: inline; font-weight: bold; } .buybox__meta .buybox__list { line-height: 1.3; } .buybox__meta .buybox__list li { position: relative; padding-left: 1em; list-style: none; margin-bottom: 5px; } .buybox__meta .buybox__list li:before { font-size: 1em; content: '\2022'; float: left; position: relative; top: .1em; font-family: serif; font-weight: 600; text-align: center; line-height: inherit; color: #666; width: auto; margin-left: -1em; } .buybox__meta .buybox__list li:last-child { margin-bottom: 0; } /*---------------------------------*/ .buybox .buybox__footer { border: 1px solid #b3b3b3; border-top: 0; padding: 8px 12px; position: relative; border-style: dashed; } /*-----------------------------------------------------------------*/ @media screen and (min-width: 460px) and (max-width: 1074px) { .buybox__body .buybox__section { display: inline-block; vertical-align: top; padding: 12px 12px; padding-bottom: 0; text-align: left; width: 48%; } .buybox__body .buybox__section { padding-top: 16px; padding-left: 0; } .buybox__section:nth-of-type(2) .buybox__meta { border-left: 1px solid #d3d3d3; padding-left: 28px; } .buybox__section:nth-of-type(2) .buybox__buttons { border-top: 0; padding-top: 0; padding-left: 16px ; } .buybox__buttons .buybox__buy-button { } /********** article buybox specific **********/ .buybox.article__buybox .buybox__section:nth-of-type(2) { margin-top: 16px; padding-top: 0; } .buybox.article__buybox .buybox__section:nth-of-type(2) .buybox__meta { margin-top: 40px; padding-top: 0; padding-bottom: 45px; } .buybox.article__buybox .buybox__section:nth-of-type(2) .buybox__meta:only-of-type { margin-top: 8px; padding-top: 12px; padding-bottom: 12px; } /********** mycopy buybox specific **********/ .buybox.mycopy__buybox .buybox__section:first-child { width: 69%; } .buybox.mycopy__buybox .buybox__section:last-child { width: 29%; } /******/ } /*-----------------------------------------------------------------*/ @media screen and (max-width: 459px) { /********** mycopy buybox specific **********/ .buybox.mycopy__buybox .buybox__body { padding-bottom: 5px; } .buybox.mycopy__buybox .buybox__section:last-child { text-align: center; width: 100%; } .buybox.mycopy__buybox .buybox__buttons { display: inline-block; width: 150px ; } /******/ } /*-----------------------------------------------------------------*/ Log in to check access Buy (PDF) EUR 34,95 Unlimited access to the full article Instant download Include local sales tax if applicable Subscribe to Journal Get Access to International Journal on Software Tools for Technology Transfer for the whole of 2017 Find out about institutional subscriptions (function () { var forEach = function (array, callback, scope) { for (var i = 0; i Export citation .RIS Papers Reference Manager RefWorks Zotero .ENW EndNote .BIB BibTeX JabRef Mendeley Share article Email Facebook Twitter LinkedIn Cookies We use cookies to improve your experience with our site. More information Accept Over 10 million scientific documents at your fingertips