TY - GEN
T1 - Construction of abstract state graphs for understanding event-B models
AU - Morita, Daichi
AU - Ishikawa, Fuyuki
AU - Honiden, Shinichi
N1 - Funding Information:
This work is partially supported by JSPS KAKENHI Grant Number 17H01727.
PY - 2017
Y1 - 2017
N2 - Event-B is a formal method that supports correctness by construction in system modeling using stepwise refinement. However, it is difficult to understand the rigorous behaviors of models from Event-B specifications, such as the reachable state space or the possible sequences of events. This is because the Event-B model is described in a style that lists events that have concurrently been enabled depending on their guard conditions. This paper proposes a method that helps in understanding the rigorous behaviors of an Event-B model by creating an abstract state graph. The core of our method involves dividing the concrete state space by using the guard conditions of individual events to extract states that are essential to enable possible transitions to be understood. Moreover, we further divided the state space by using the guard conditions of events in the models before refinement to support understanding of changes in behaviors between the models before and after refinement. Our unique approach facilitated finding of invariants that were not specified but held, which were useful for validation.
AB - Event-B is a formal method that supports correctness by construction in system modeling using stepwise refinement. However, it is difficult to understand the rigorous behaviors of models from Event-B specifications, such as the reachable state space or the possible sequences of events. This is because the Event-B model is described in a style that lists events that have concurrently been enabled depending on their guard conditions. This paper proposes a method that helps in understanding the rigorous behaviors of an Event-B model by creating an abstract state graph. The core of our method involves dividing the concrete state space by using the guard conditions of individual events to extract states that are essential to enable possible transitions to be understood. Moreover, we further divided the state space by using the guard conditions of events in the models before refinement to support understanding of changes in behaviors between the models before and after refinement. Our unique approach facilitated finding of invariants that were not specified but held, which were useful for validation.
UR - http://www.scopus.com/inward/record.url?scp=85032683925&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=85032683925&partnerID=8YFLogxK
U2 - 10.1007/978-3-319-69483-2_15
DO - 10.1007/978-3-319-69483-2_15
M3 - Conference contribution
AN - SCOPUS:85032683925
SN - 9783319694825
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 250
EP - 265
BT - Dependable Software Engineering
A2 - Wang, Ji
A2 - Larsen, Kim Guldstrand
A2 - Sokolsky, Oleg
PB - Springer Verlag
T2 - 3rd International Symposium on Dependable Software Engineering: Theories, Tools and Applications, SETTA 2017
Y2 - 23 October 2017 through 25 October 2017
ER -