Abstract
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.
This work is partially supported by JSPS KAKENHI Grant Number 17H01727.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
References
Abrial, J.R.: Modeling in Event-B: System and Software Engineering. Cambridge University Press, New York (2010)
Abrial, J.R., Butler, M., Hallerstede, S., Hoang, T.S., Mehta, F., Voisin, L.: Rodin: an open toolset for modelling and reasoning in Event-B. Int. J. Softw. Tools Technol. Transf. (STTT) 12(6), 447–466 (2010)
Barrett, C., Sebastiani, R., Seshia, S., Tinelli, C.: Satisfiability modulo theories. In: Handbook of Satisfiability, Frontiers in Artificial Intelligence and Applications, vol. 185, Chap. 26, pp. 825–885. IOS Press (2009)
Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, Cambridge (1999)
de Moura, L., Bjørner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337–340. Springer, Heidelberg (2008). doi:10.1007/978-3-540-78800-3_24
Dulac, N., Viguier, T., Leveson, N.G., Storey, M.D.: On the use of visualization in formal requirements specification. In: Proceedings of the IEEE Joint International Conference on Requirements Engineering, pp. 71–80 (2002)
Gabbay, D., Pnueli, A., Shelah, S., Stavi, J.: On the temporal analysis of fairness. In: Proceedings of the 7th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 1980), pp. 163–173. ACM, New York (1980)
Graf, S., Saidi, H.: Construction of abstract state graphs with PVS. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol. 1254, pp. 72–83. Springer, Heidelberg (1997). doi:10.1007/3-540-63166-6_10
Ham, F.V., van de Wetering, H., Van Wijk, J.J.: Visualization of state transition graphs. In: Proceedings of the IEEE Symposium on Information Visualization 2001 (INFOVIS 2001), p. 59. IEEE Computer Society, Washington, DC (2001)
Hoang, T.S., Schneider, S., Treharne, H., Williams, D.M.: Foundations for using linear temporal logic in Event-B refinement. Form. Aspects Comput. 28(6), 909–935 (2016)
Ladenberger, L., Leuschel, M.: Mastering the visualization of larger state spaces with projection diagrams. In: Butler, M., Conchon, S., Zaïdi, F. (eds.) ICFEM 2015. LNCS, vol. 9407, pp. 153–169. Springer, Cham (2015). doi:10.1007/978-3-319-25423-4_10
Leuschel, M., Butler, M.: ProB: an automated analysis toolset for the B method. Int. J. Softw. Tools Technol. Transf. 10(2), 185–203 (2008)
Leuschel, M., Turner, E.: Visualising larger state spaces in PRO B. In: Treharne, H., King, S., Henson, M., Schneider, S. (eds.) ZB 2005. LNCS, vol. 3455, pp. 6–23. Springer, Heidelberg (2005). doi:10.1007/11415787_2
Lichtenstein, O., Pnueli, A.: Checking that finite state concurrent programs satisfy their linear specification. In: Proceedings of the 12th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages (POPL 1985), pp. 97–107. ACM, New York (1985)
Plagge, D., Leuschel, M.: Seven at one stroke: LTL model checking for high-level specifications in B, Z, CSP, and more. Int. J. Softw. Tools Technol. Transf. 12(1), 9–21 (2010)
Snook, C., Butler, M.: UML-B and Event-B: an integration of languages and tools. In: Proceedings of the IASTED International Conference on Software Engineering (SE 2008), pp. 336–341. ACTA Press, Anaheim (2008)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
A Appendix
A Appendix
This appendix explains how we investigated the advanced and unique use described in Subsects. 3.5 and 4.4 to discover invariants that were stronger than the invariants described in the specifications by using a graph constructed with CASG. We used the Mac2 model and the specifications are in Abrial [1, Chap. 2].
We applied the first method and discovered three unreachable states from the graph. One of them is represented by
We then tried to add the predicate
as an invariant to the Mac2 model on the Rodin platform [2]. As proof obligation is automatically discharged by them, the predicate is actually an invariant of the model. This invariant is equivalent to:
which means that if all the traffic lights are red, the flags are true and there are no cars on the bridge, then the number of cars on the island is zero or has reached its capacity. Developers can check if the situation is valid in the model.
We investigated the number of transitions in the Mac2 graph constructed by using CASG that could occur in the second method. We specified the range of the constant d from one to 10 because it seemed to be sufficient from our investigation of the model. We checked all 58 edges in the graph and discovered 16 edges that did not actually occur. One of them was the transition labeled \(IL\_in\) from the abstract state represented by:
to another represented by:
A concrete state where the transition can occur is:
However, it is actually unreachable because the condition \(ml\_pass = false\) requires the event \(ML\_tl\_green\) to occur and \(ML\_out\_1\) and \(ML\_out\_2\) must not subsequently occur. There was some suggestion that the model always satisfies \(a>0 \Rightarrow ml\_pass=true\) because \(a>0\) means \(ML\_out\_1\) or \(ML\_out\_2\) has occurred at least once just after \(ML\_tl\_green\) has taken place. Then, we added it as an invariant to the Rodin platform, but its proof obligation was not automatically discharged. Due to an analysis of the failure of the proof, which is often used in Event-B, we added \((ml\_tl=red \wedge a+b \ne d) \Rightarrow a = 0\) as an invariant and all proof obligations were automatically discharged.
Finally, let us take Mac2 as an example of the third method. The abstract state represented by the predicate (1) does not satisfy the condition. All the transitions into it are labeled \(ML\_tl\_green\). Since \(ML\_tl\_green\) makes \(ml\_pass\) false, all concrete states where \(ml\_pass\) is true in the abstract state are unreachable. There was some suggestion that the predicate \(a=b=0 \wedge ml\_tl = green \Rightarrow ml\_pass = false\) was an invariant. Therefore, we added it and proof obligation was discharged.
Rights and permissions
Copyright information
© 2017 Springer International Publishing AG
About this paper
Cite this paper
Morita, D., Ishikawa, F., Honiden, S. (2017). Construction of Abstract State Graphs for Understanding Event-B Models. In: Larsen, K., Sokolsky, O., Wang, J. (eds) Dependable Software Engineering. Theories, Tools, and Applications. SETTA 2017. Lecture Notes in Computer Science(), vol 10606. Springer, Cham. https://doi.org/10.1007/978-3-319-69483-2_15
Download citation
DOI: https://doi.org/10.1007/978-3-319-69483-2_15
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-69482-5
Online ISBN: 978-3-319-69483-2
eBook Packages: Computer ScienceComputer Science (R0)