Skip to main content
SpringerLink
Log in

Graphic Modelling Approach as a Support for Event-B Modelling

  • Conference paper
  • First Online:
Proceedings of 2017 Chinese Intelligent Systems Conference (CISC 2017)

Part of the book series: Lecture Notes in Electrical Engineering ((LNEE,volume 459))

Included in the following conference series:

Abstract

Event-B method, as an evolution of B-method, is a formal method for system-level modelling and analysis based on extended first order logic and set theory, which provides flexible approaches of refinement and decomposition to construct large systems gradually with some successful applications in their formal verifications. However, it is hard to manipulate and grasp this method for many researchers because of its highly abstraction. In order to reduce the burden of developers’ work and the complexity of Event-B model, a graphic modeling approach, called Event-B graph, is introduced in this paper, which is used as an alternative way to clearly describe the state flow of the model and provide a graphic way of system-level modelling to bridge the real problem and the Event-B model construction. After introducing some new concepts and structure of Event-B graph, the transformation algorithm from Event-B graph to Event-B model is provided and the equivalence of the transformation is then proved. An example is finally provided to illustrate the procedure of Event-B graph construction.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 169.00
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 219.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info
Hardcover Book
USD 219.99
Price excludes VAT (USA)
  • Durable hardcover edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Similar content being viewed by others

References

  1. Cansell Dominique, Méry Dominique. The Event-B method—concept and case studies. Monographs in Theoretical Computer Science, Berlin: Springer; 2008. p. 47–152.

    Google Scholar 

  2. Abrial J -R, Hallerstede S. Refinement, decomposition, and instantiation of discrete models: application to Event-B. In: International workshop on abstract state machine, vol. 77, no. 1–2; 2007; p. 17–40.

    Google Scholar 

  3. Kobayashi T, Ishikawa F, Honiden S. Refactoring refinement structure of Event-B machine. Springer International Publishing AG;2016. p. 444–59.

    Google Scholar 

  4. A Edmunds, C Snook, M Walden. On Component-Based Reuse for Event-B [C]. International Conference on Abstract State Machines;2016: 151–166.

    Google Scholar 

  5. Dghaym D, Trindade MG, Bulter M, Fathabali AS. In: A graphical tool for Event-B refinement structure. Abstract state machines, alloy, B, Tla, VDM, and Z: international conference;2016.

    Google Scholar 

  6. C. Métayer (ClearSy), J.-R. Abrial, L. Voisin (ETH Zürich). Event-B language [EB/OL]. http://rodin.cs.ncl.ac.uk/;2005.

  7. Alur R, Dill DL. A Theory of Timed Automata [J]. Theoret Comput Sci. 1994;126(2):183–235.

    Article  MathSciNet  MATH  Google Scholar 

  8. Abrial JR, Lee MKO, Neilson D, Scharbach PN, Sorensen IH. The B-mehod. In: Vdm 91-formal software development, international symposium of Vdm Europe, vol. 552, no. 1;1991. p. 398–405

    Google Scholar 

  9. Dghaym D, Trindade MG, Bulter M, Fathabali AS. A graphical tool for Event-B refinement structure. In: abstract state machines, Alloy, B, Tla, VDM, and Z: international conference;2016. p. 269–74.

    Google Scholar 

  10. Abrial J -R, Butler MJ, Hallerstede S, Voisin L. A Roadmap for the rodin toolset. German: Springe;2008. p. 347–47.

    Google Scholar 

  11. Thai Son Hoang. Steve Schneider, Helen Treharne and David M. Williams. Reasoning about Action System Using the B-Method [J]. Formal Aspects Comput. 2016;28(6):1–27.

    MathSciNet  Google Scholar 

  12. Said MY, Butler MJ, Snook CF. Language and tool support for class and state machine refinement in UML-B. In: World Congress on Formal Methods;2009. p. 579–95.

    Google Scholar 

  13. Iliasov A. Use case scenarios as verification conditions: Event-B/Flow approach; 2011, 8968: 9–23.

    Google Scholar 

  14. Schneider S, Treharne H, Wehrheim H. The behavioural semantics of Event-B refinement. Formal Aspects Comput. 2014; 26(2):251–80.

    Google Scholar 

  15. Abrial J-R. Modeling in Event-B: system and software engineering. New York: Cambridge University Press; 2010. p. 100–48.

    Book  MATH  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. National Local Joint Engineering Laboratory of System Credibility Automatic Verification, School of Mathematics, Southwest Jiaotong University, Chengdu, 610031, Sichuan, China

    Xiaolong Li, Jun Liu, Keming Wang & Yang Xu

  2. School of Computing and Mathematics, Ulster University, Belfast, Northern Ireland, UK

    Jun Liu

Authors
  1. Xiaolong Li
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Jun Liu
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Keming Wang
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Yang Xu
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Xiaolong Li .

Editor information

Editors and Affiliations

  1. Beihang University , Beijing, China

    Yingmin Jia

  2. Beijing University of Posts and Telecommunications, Beijing, China

    Junping Du

  3. University of Science and Technology Beijing, Beijing, China

    Weicun Zhang

Rights and permissions

Reprints and permissions

Copyright information

© 2018 Springer Nature Singapore Pte Ltd.

About this paper

Cite this paper

Li, X., Liu, J., Wang, K., Xu, Y. (2018). Graphic Modelling Approach as a Support for Event-B Modelling. In: Jia, Y., Du, J., Zhang, W. (eds) Proceedings of 2017 Chinese Intelligent Systems Conference. CISC 2017. Lecture Notes in Electrical Engineering, vol 459. Springer, Singapore. https://doi.org/10.1007/978-981-10-6496-8_59

Download citation

  • DOI: https://doi.org/10.1007/978-981-10-6496-8_59

  • Published:

  • Publisher Name: Springer, Singapore

  • Print ISBN: 978-981-10-6495-1

  • Online ISBN: 978-981-10-6496-8

  • eBook Packages: EngineeringEngineering (R0)

Publish with us

Policies and ethics

Search

Navigation