Extracting Traceability between Predicates in Event-B Refinement

Shinnosuke Saruwatari, Fuyuki Ishikawa, Tsutomu Kobayashi, Shinichi Honiden

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

1 Citation (Scopus)

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 languageEnglish
Title of host publicationProceedings - 24th Asia-Pacific Software Engineering Conference, APSEC 2017
PublisherIEEE Computer Society
Pages61-70
Number of pages10
Volume2017-December
ISBN (Electronic)9781538636817
DOIs
Publication statusPublished - 2018 Mar 1
Externally publishedYes
Event24th Asia-Pacific Software Engineering Conference, APSEC 2017 - Nanjing, Jiangsu, China
Duration: 2017 Dec 42017 Dec 8

Other

Other24th Asia-Pacific Software Engineering Conference, APSEC 2017
CountryChina
CityNanjing, Jiangsu
Period17/12/417/12/8

Fingerprint

Engineers
Reverse engineering
Refining
Concretes

Keywords

  • Event-B
  • Formal Method
  • Refinement
  • Reverse Engineering

ASJC Scopus subject areas

  • Software

Cite this

Saruwatari, S., Ishikawa, F., Kobayashi, T., & Honiden, S. (2018). Extracting Traceability between Predicates in Event-B Refinement. In Proceedings - 24th Asia-Pacific Software Engineering Conference, APSEC 2017 (Vol. 2017-December, pp. 61-70). IEEE Computer Society. https://doi.org/10.1109/APSEC.2017.12

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 proceedingConference contribution

Saruwatari, S, Ishikawa, F, Kobayashi, T & Honiden, S 2018, Extracting Traceability between Predicates in Event-B Refinement. in Proceedings - 24th Asia-Pacific Software Engineering Conference, APSEC 2017. vol. 2017-December, IEEE Computer Society, pp. 61-70, 24th Asia-Pacific Software Engineering Conference, APSEC 2017, Nanjing, Jiangsu, China, 17/12/4. https://doi.org/10.1109/APSEC.2017.12
Saruwatari S, Ishikawa F, Kobayashi T, Honiden S. Extracting Traceability between Predicates in Event-B Refinement. In Proceedings - 24th Asia-Pacific Software Engineering Conference, APSEC 2017. Vol. 2017-December. IEEE Computer Society. 2018. p. 61-70 https://doi.org/10.1109/APSEC.2017.12
Saruwatari, Shinnosuke ; Ishikawa, Fuyuki ; Kobayashi, Tsutomu ; Honiden, Shinichi. / Extracting Traceability between Predicates in Event-B Refinement. Proceedings - 24th Asia-Pacific Software Engineering Conference, APSEC 2017. Vol. 2017-December IEEE Computer Society, 2018. pp. 61-70
@inproceedings{5bd8c91e896c4425ae3a61d791d4cf25,
title = "Extracting Traceability between Predicates in Event-B Refinement",
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.",
keywords = "Event-B, Formal Method, Refinement, Reverse Engineering",
author = "Shinnosuke Saruwatari and Fuyuki Ishikawa and Tsutomu Kobayashi and Shinichi Honiden",
year = "2018",
month = "3",
day = "1",
doi = "10.1109/APSEC.2017.12",
language = "English",
volume = "2017-December",
pages = "61--70",
booktitle = "Proceedings - 24th Asia-Pacific Software Engineering Conference, APSEC 2017",
publisher = "IEEE Computer Society",

}

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 -