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 language | English |
|---|---|
| Title of host publication | Abstract State Machines, Alloy, B, TLA, VDM, and Z - 4th International Conference, ABZ 2014, Proceedings |
| Publisher | Springer-Verlag |
| Pages | 277-283 |
| Number of pages | 7 |
| ISBN (Print) | 9783662436516 |
| DOIs | |
| Publication status | Published - 2014 Jan 1 |
| Externally published | Yes |
| Event | 4th International Conference on Abstract State Machines, Alloy, B, TLA, VDM, and Z, ABZ 2014 - Toulouse, France Duration: 2014 Jun 2 → 2014 Jun 6 |
Publication series
| Name | Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) |
|---|---|
| Volume | 8477 LNCS |
| ISSN (Print) | 0302-9743 |
| ISSN (Electronic) | 1611-3349 |
Other
| Other | 4th International Conference on Abstract State Machines, Alloy, B, TLA, VDM, and Z, ABZ 2014 |
|---|---|
| Country | France |
| City | Toulouse |
| Period | 14/6/2 → 14/6/6 |
Fingerprint
ASJC Scopus subject areas
- Computer Science(all)
- Theoretical Computer Science
Cite this
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 proceeding › Conference contribution
}
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 -