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
Externally publishedYes
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

Event-B
Large scale systems
Refinement
Planning
Specifications
Formal Specification
Intuitive
Complex Systems
Eliminate
Valid
Specification
Formal specification

ASJC Scopus subject areas

  • Computer Science(all)
  • Theoretical Computer Science

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

Understanding and planning Event-B refinement through primitive rationales. / Kobayashi, Tsutomu; Ishikawa, Fuyuki; Honiden, Shinichi.

Abstract State Machines, Alloy, B, TLA, VDM, and Z - 4th International Conference, ABZ 2014, Proceedings. Springer-Verlag, 2014. p. 277-283 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 8477 LNCS).

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

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. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 8477 LNCS, Springer-Verlag, pp. 277-283, 4th International Conference on Abstract State Machines, Alloy, B, TLA, VDM, and Z, ABZ 2014, Toulouse, France, 14/6/2. https://doi.org/10.1007/978-3-662-43652-3_24
Kobayashi T, Ishikawa F, Honiden S. 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. Springer-Verlag. 2014. p. 277-283. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). https://doi.org/10.1007/978-3-662-43652-3_24
Kobayashi, Tsutomu ; Ishikawa, Fuyuki ; Honiden, Shinichi. / Understanding and planning Event-B refinement through primitive rationales. Abstract State Machines, Alloy, B, TLA, VDM, and Z - 4th International Conference, ABZ 2014, Proceedings. Springer-Verlag, 2014. pp. 277-283 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).
@inproceedings{c149dfa37a5b4c90816db56cc1f37c8f,
title = "Understanding and planning Event-B refinement through primitive rationales",
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.",
author = "Tsutomu Kobayashi and Fuyuki Ishikawa and Shinichi Honiden",
year = "2014",
month = "1",
day = "1",
doi = "10.1007/978-3-662-43652-3_24",
language = "English",
isbn = "9783662436516",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer-Verlag",
pages = "277--283",
booktitle = "Abstract State Machines, Alloy, B, TLA, VDM, and Z - 4th International Conference, ABZ 2014, Proceedings",

}

TY - GEN

T1 - Understanding and planning Event-B refinement through primitive rationales

AU - Kobayashi, Tsutomu

AU - Ishikawa, Fuyuki

AU - Honiden, Shinichi

PY - 2014/1/1

Y1 - 2014/1/1

N2 - 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.

AB - 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.

UR - http://www.scopus.com/inward/record.url?scp=84903557809&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=84903557809&partnerID=8YFLogxK

U2 - 10.1007/978-3-662-43652-3_24

DO - 10.1007/978-3-662-43652-3_24

M3 - Conference contribution

SN - 9783662436516

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 277

EP - 283

BT - Abstract State Machines, Alloy, B, TLA, VDM, and Z - 4th International Conference, ABZ 2014, Proceedings

PB - Springer-Verlag

ER -