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/semiformal 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. |
Year | DOI | Venue |
---|---|---|
2014 | 10.1007/978-3-662-43652-3_24 | ABZ |
Field | DocType | Volume |
Consistency rules,Software engineering,Computer science,Formal specification,Management science | Conference | 8477 |
ISSN | Citations | PageRank |
0302-9743 | 2 | 0.39 |
References | Authors | |
6 | 3 |
Name | Order | Citations | PageRank |
---|---|---|---|
Tsutomu Kobayashi | 1 | 7 | 2.92 |
Fuyuki Ishikawa | 2 | 501 | 51.34 |
Shinichi Honiden | 3 | 1172 | 139.69 |