Abstract
ProB is an animator and model checker for the B method. It also allows to visualise the state space of a B machine in graphical way. This is often very useful and allows users to quickly spot whether the machine behaves as expected. However, for larger state spaces the visualisation quickly becomes difficult to grasp by users (and the computation of the graph layout takes considerable time). In this paper we present two relatively simple algorithms to often considerably reduce the complexity of the graphs, while still kee** relevant information. This makes it possible to visualise much larger state spaces and gives the user immediate feedback about the overall behaviour of a machine. The algorithms have been implemented within the ProB toolset and we highlight their potential on several examples. We also conduct a thorough experimentation of the algorithm on 47 B machines and analyse the results.
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
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Abrial, J.-R.: The B-Book. Cambridge University Press, Cambridge (1996)
Aho, A.V., Sethi, R., Ullman, J.D.: Compilers — Principles, Techniques and Tools. Addison-Wesley, Reading (1986)
Ambert, F., Bouquet, F., Chemin, S., Guenaud, S., Legeard, B., Peureux, F., Utting, M., Vacelet, N.: BZ-testing-tools: A tool-set for test generation from Z and B using constraint logic programming. In: Proceedings of FATES 2002, Formal Approaches to Testing of Software. Technical Report, INRIA, August 2002, pp. 105–120 (2002)
AT&T Labs-Research. Graphviz - open source graph drawing software. Obtainable at, http://www.research.att.com/sw/tools/graphviz/
B-Core (UK) Limited, Oxon, UK. B-Toolkit, On-line manual(1999), Available at, http://www.b-core.com/ONLINEDOC/Contents.html
Bensalem, S., Lakhnech, Y., Owre, S.: Computing abstractions of infinite state systems compositionally and automatically. In: Y. Vardi, M. (ed.) CAV 1998. LNCS, vol. 1427, pp. 319–331. Springer, Heidelberg (1998)
Bouquet, F., Legeard, B., Peureux, F.: CLPS-B - a constraint solver for B. In: Katoen, J.-P., Stevens, P. (eds.) TACAS 2002. LNCS, vol. 2280, pp. 188–204. Springer, Heidelberg (2002)
Casner, S., Larkin, J.: Cognitive Efficiency Considerations for Good Graphic Design. In: 11th Annual Conf. of the Cognitive Science Society, Ann Arbor, Michigan (August 1989)
Clarke, E.M., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (1999)
Ham, H.W.F., Wijk, J.: Visualization of State Transition Graphs. In: IEEE Symposium on Information Visualization, San Diego, CA, USA, October 2001, pp. 59–63 (2001)
Fitter, M., Green, T.: When Do Diagrams Make Good Programming Languages? Int. Journal of Man-Machine Studies, 235–261 (1979)
Groote, J., Ham, F.: Large State Space Visualization. In: Garavel, H., Hatcliff, J. (eds.) TACAS 2003. LNCS, vol. 2619, pp. 585–590. Springer, Heidelberg (2003)
Herman, I., Melanon, G., Marshall, M.S.: Graph Visualization and Navigation in Information Visualization: A Survey. IEEE Transactions on Visualization and Computer Graphics 6(1), 24–43 (2000)
Hopcroft, J.E., Ullman, J.D.: Introduction to Automata Theory, Languages and Computation. Addison-Wesley, Reading (1979)
Ilie, L., Yu, S.: Algorithms for Computing Small NFAs. In: Diks, K., Rytter, W. (eds.) MFCS 2002. LNCS, vol. 2420, p. 328. Springer, Heidelberg (2002)
Jiang, T., Ravikunar, B.: Minimal NFA Problems are Hard. SIAM Journal on Computing 22(6), 1117–1141 (1993)
John, S.A.: Minimal Unambigous ε-NFA. In: Domaratzki, M., Okhotin, A., Salomaa, K., Yu, S. (eds.) CIAA 2004. LNCS, vol. 3317, pp. 190–201. Springer, Heidelberg (2005)
Leuschel, M., Butler, M.: ProB: A model checker for B. In: Araki, K., Gnesi, S., Mandrioli, D. (eds.) FME 2003. LNCS, vol. 2805, pp. 855–874. Springer, Heidelberg (2003)
Leuschel, M., Turner, E.: Visualising larger states spaces in ProB. Technical report, School of Electronics and Computer Science, University of Southampton (January 2005)
Malcher, A.: Minimizing Finite Automata is Computationally Hard. In: Ésik, Z., Fülöp, Z. (eds.) DLT 2003. LNCS, vol. 2710, pp. 386–397. Springer, Heidelberg (2003)
Dulac, N.L.N., Viguier, T., Storey, M.-A.: On the use of Visualization in Formal Requirements Specification. In: IEEE Joint International Conference on Requirements Engineering, Essen, Germany, September 2002, pp. 71–81 (2002)
Rusu, V., Singerman, E.: On proving safety properties by integrating static analysis, theorem proving and abstraction. In: Cleaveland, W.R. (ed.) TACAS 1999. LNCS, vol. 1579, p. 178. Springer, Heidelberg (1999)
Sadi, H., Shankar, N.: Abstract and model check while you prove. In: Halbwachs, N., Peled, D.A. (eds.) CAV 1999. LNCS, vol. 1633, pp. 319–331. Springer, Heidelberg (1999)
Steria, Aix-en-Provence, France. Atelier B, User and Reference Manuals (1996) Available at, http://www.atelierb.societe.com/index_uk.html
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2005 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Leuschel, M., Turner, E. (2005). Visualising Larger State Spaces in Pro B . In: Treharne, H., King, S., Henson, M., Schneider, S. (eds) ZB 2005: Formal Specification and Development in Z and B. ZB 2005. Lecture Notes in Computer Science, vol 3455. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11415787_2
Download citation
DOI: https://doi.org/10.1007/11415787_2
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-25559-8
Online ISBN: 978-3-540-32007-4
eBook Packages: Computer ScienceComputer Science (R0)