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/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 Kobayashi172.92
Fuyuki Ishikawa250151.34
Shinichi Honiden31172139.69