Understanding and planning Event-B refinement through primitive rationales

Tsutomu Kobayashi, Fuyuki Ishikawa, Shinichi Honiden

Research output: Chapter in Book/Report/Conference proceedingConference contribution

2 Citations (Scopus)

Abstract

Event-B provides a promising feature of refinement to gradually construct a comprehensive specification of a complex system including various aspects. It has unique difficulties to design complexity mitigation, while obeying Event-B consistency rules, among the potentially large possibilities of refinement plans. However, despite of the difficulties, existing studies on specific examples or high-level and intuitive guidelines are missing clear rationales, as well as principles, guidelines or methods supported by the rationales. In response to this problem, this paper presents a method for refinement planning from an informal/semi-formal specification. By defining primitive rationales, the method can eliminate undesirable plans such as the ones failing to mitigate the complexity. In a case study on a popular example from a book, we derived an enough small number of valid plans only by using the general and essential rationales while explaining the one presented in the book.

Original languageEnglish
Title of host publicationAbstract State Machines, Alloy, B, TLA, VDM, and Z - 4th International Conference, ABZ 2014, Proceedings
PublisherSpringer Verlag
Pages277-283
Number of pages7
ISBN (Print)9783662436516
DOIs
Publication statusPublished - 2014 Jan 1
Event4th International Conference on Abstract State Machines, Alloy, B, TLA, VDM, and Z, ABZ 2014 - Toulouse, France
Duration: 2014 Jun 22014 Jun 6

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume8477 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Other

Other4th International Conference on Abstract State Machines, Alloy, B, TLA, VDM, and Z, ABZ 2014
CountryFrance
CityToulouse
Period14/6/214/6/6

    Fingerprint

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Cite this

Kobayashi, T., Ishikawa, F., & Honiden, S. (2014). Understanding and planning Event-B refinement through primitive rationales. In Abstract State Machines, Alloy, B, TLA, VDM, and Z - 4th International Conference, ABZ 2014, Proceedings (pp. 277-283). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 8477 LNCS). Springer Verlag. https://doi.org/10.1007/978-3-662-43652-3_24