Abstract
Event-B requires engineers to satisfy proof obligations and inherit all predicates from abstract models while constructing concrete ones. Engineers typically derive predicates from abstract models through transformation with the intention of gradually refining the models. These kinds of intentions for refinement are essential for other engineers to understand the refinements. However, these are implicit and not directly specified in the models. Therefore, it is difficult to understand how each predicate in concrete models is obtained from the predicates in abstract models. This paper proposes an effective method of extracting these relationships. Our approach uses heuristics to avoid exhaustive matching between predicates. It tries to find a set of related predicates by tracing elements, such as variables and constants in predicates, and excluding predicates that use common variables, but differently. Our method facilitates understanding of the intentions of refinements and can be used to help reverse engineering by clarifying the relationships between predicates through refinements.
| Original language | English |
|---|---|
| Title of host publication | Proceedings - 24th Asia-Pacific Software Engineering Conference, APSEC 2017 |
| Publisher | IEEE Computer Society |
| Pages | 61-70 |
| Number of pages | 10 |
| Volume | 2017-December |
| ISBN (Electronic) | 9781538636817 |
| DOIs | |
| Publication status | Published - 2018 Mar 1 |
| Externally published | Yes |
| Event | 24th Asia-Pacific Software Engineering Conference, APSEC 2017 - Nanjing, Jiangsu, China Duration: 2017 Dec 4 → 2017 Dec 8 |
Other
| Other | 24th Asia-Pacific Software Engineering Conference, APSEC 2017 |
|---|---|
| Country | China |
| City | Nanjing, Jiangsu |
| Period | 17/12/4 → 17/12/8 |
Fingerprint
Keywords
- Event-B
- Formal Method
- Refinement
- Reverse Engineering
ASJC Scopus subject areas
- Software
Cite this
Extracting Traceability between Predicates in Event-B Refinement. / Saruwatari, Shinnosuke; Ishikawa, Fuyuki; Kobayashi, Tsutomu; Honiden, Shinichi.
Proceedings - 24th Asia-Pacific Software Engineering Conference, APSEC 2017. Vol. 2017-December IEEE Computer Society, 2018. p. 61-70.Research output: Chapter in Book/Report/Conference proceeding › Conference contribution
}
TY - GEN
T1 - Extracting Traceability between Predicates in Event-B Refinement
AU - Saruwatari, Shinnosuke
AU - Ishikawa, Fuyuki
AU - Kobayashi, Tsutomu
AU - Honiden, Shinichi
PY - 2018/3/1
Y1 - 2018/3/1
N2 - Event-B requires engineers to satisfy proof obligations and inherit all predicates from abstract models while constructing concrete ones. Engineers typically derive predicates from abstract models through transformation with the intention of gradually refining the models. These kinds of intentions for refinement are essential for other engineers to understand the refinements. However, these are implicit and not directly specified in the models. Therefore, it is difficult to understand how each predicate in concrete models is obtained from the predicates in abstract models. This paper proposes an effective method of extracting these relationships. Our approach uses heuristics to avoid exhaustive matching between predicates. It tries to find a set of related predicates by tracing elements, such as variables and constants in predicates, and excluding predicates that use common variables, but differently. Our method facilitates understanding of the intentions of refinements and can be used to help reverse engineering by clarifying the relationships between predicates through refinements.
AB - Event-B requires engineers to satisfy proof obligations and inherit all predicates from abstract models while constructing concrete ones. Engineers typically derive predicates from abstract models through transformation with the intention of gradually refining the models. These kinds of intentions for refinement are essential for other engineers to understand the refinements. However, these are implicit and not directly specified in the models. Therefore, it is difficult to understand how each predicate in concrete models is obtained from the predicates in abstract models. This paper proposes an effective method of extracting these relationships. Our approach uses heuristics to avoid exhaustive matching between predicates. It tries to find a set of related predicates by tracing elements, such as variables and constants in predicates, and excluding predicates that use common variables, but differently. Our method facilitates understanding of the intentions of refinements and can be used to help reverse engineering by clarifying the relationships between predicates through refinements.
KW - Event-B
KW - Formal Method
KW - Refinement
KW - Reverse Engineering
UR - http://www.scopus.com/inward/record.url?scp=85045884638&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=85045884638&partnerID=8YFLogxK
U2 - 10.1109/APSEC.2017.12
DO - 10.1109/APSEC.2017.12
M3 - Conference contribution
AN - SCOPUS:85045884638
VL - 2017-December
SP - 61
EP - 70
BT - Proceedings - 24th Asia-Pacific Software Engineering Conference, APSEC 2017
PB - IEEE Computer Society
ER -