Abstract
A domain specific visualisation can greatly contribute to better understanding of formal models. In this work we propose an approach that supports the user in creating domain specific visualisations of CSP models. CSP (Communicating Sequential Processes) is a formal language that is mainly used for specifying concurrent and distributed systems. We have successfully created various visualisations of CSP models in order to demonstrate our approach. The visualisations of two case studies are presented in this paper: the bully algorithm and a level crossing gate. In addition, we discuss possible applications of our approach.
The work in this paper is partly funded by ADVANCE, an European Commission Information and Communication Technologies FP7 project.
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
Notes
- 1.
The new version of BMotion Studio is not officially released yet, but the source code is available from http://www.stups.hhu.de/bmotionstudio/index.php/Source.
- 2.
For more information about jQuery and selectors we refer the reader to the jQuery API documentation http://api.jquery.com/category/selectors/.
- 3.
The node with ID 0 can never be a coordinator as there is no node with a lower ID.
References
ADVANCE Deliverable D4.2 (Issue 2). Methods and tools for simulation and testing I, March 2013
ECMA-404 The JSON Data Interchange Standard. Ecma International, October 2013
Abrial, J.: Modeling in Event-B: System and Software Engineering. Cambridge University Press, New York (2010)
Bendisposto, J., Leuschel, M.: A generic flash-based animation engine for ProB. In: Julliand, J., Kouchnarenko, O. (eds.) B 2007. LNCS, vol. 4355, pp. 266–269. Springer, Heidelberg (2006)
Formal Systems (Europe) Ltd., Process Behaviour Explorer (ProBE User Manual, version 1.30). http://www.fsel.com/probe_manual.html
Hansen, D., Ladenberger, L., Wiegard, H., Bendisposto, J., Leuschel, M.: Validation of the ABZ landing gear system using ProB. In: Boniol, F., Wiels, V., Ait Ameur, Y., Schewe, K.-D. (eds.) ABZ 2014. CCIS, vol. 433, pp. 66–79. Springer, Heidelberg (2014)
Hansen, D., Leuschel, M.: Translating TLA\(^ \text{+ } \) to B for validation with ProB. In: Derrick, J., Gnesi, S., Latella, D., Treharne, H. (eds.) IFM 2012. LNCS, vol. 7321, pp. 24–38. Springer, Heidelberg (2012)
Ladenberger, L., Bendisposto, J., Leuschel, M.: Visualising event-B models with B-motion studio. In: Alpuente, M., Cook, B., Joubert, C. (eds.) FMICS 2009. LNCS, vol. 5825, pp. 202–204. Springer, Heidelberg (2009)
Leuschel, M., Butler, M.: ProB: an automated analysis toolset for the B method. STTT 10(2), 185–203 (2008)
Leuschel, M., Fontaine, M.: Probing the depths of CSP-M: a new fdr-compliant validation tool. In: Liu, S., Araki, K. (eds.) ICFEM 2008. LNCS, vol. 5256, pp. 278–297. Springer, Heidelberg (2008)
Ng, M.Y., Butler, M.: Tool support for visualizing CSP in UML. In: George, C.W., Miao, H. (eds.) ICFEM 2002. LNCS, vol. 2495, pp. 287–298. Springer, Heidelberg (2002)
Plagge, D., Leuschel, M.: Validating Z specifications using the ProB animator and model checker. In: Davies, J., Gibbons, J. (eds.) IFM 2007. LNCS, vol. 4591, pp. 480–500. Springer, Heidelberg (2007)
Roscoe, A.: Understanding Concurrent Systems, 1st edn. Springer-Verlag New York Inc., New York (2010)
Roscoe, A.W., Hoare, C.A.R., Bird, R.: The Theory and Practice of Concurrency. Prentice Hall PTR, Upper Saddle River (1997)
Scattergood, B., Armstrong, P.: CSP-M: A Reference Manual (2011)
Servat, T.: BRAMA: a new graphic animation tool for B models. In: Julliand, J., Kouchnarenko, O. (eds.) B 2007. LNCS, vol. 4355, pp. 274–276. Springer, Heidelberg (2006)
Sun, J., Liu, Y., Dong, J.S., Chen, C.: Integrating specification and programs for system modeling and verification. In: Chin, W.-N., Qin, S. (eds.) Proceedings TASE 2009, pp. 127–135. IEEE Computer Society (2009)
Sun, J., Liu, Y., Dong, J.S., Pang, J.: PAT: towards flexible verification under fairness. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 709–714. Springer, Heidelberg (2009)
Gibson-Robinson, T., Armstrong, P., Boulgakov, A., Roscoe, A.W.: FDR3 — a modern refinement checker for CSP. In: Ábrahám, E., Havelund, K. (eds.) TACAS 2014 (ETAPS). LNCS, vol. 8413, pp. 187–201. Springer, Heidelberg (2014)
W3C CSS Working Group. Cascading Style Sheets (CSS) Snapshot 2010. http://www.w3.org/TR/css-2010/, May 2011
W3C SVG Working Group. Scalable Vector Graphics (SVG) 1.1 (Second Edition), August 2011. http://www.w3.org/TR/SVG11/
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2015 Springer International Publishing Switzerland
About this paper
Cite this paper
Ladenberger, L., Dobrikov, I., Leuschel, M. (2015). An Approach for Creating Domain Specific Visualisations of CSP Models. In: Canal, C., Idani, A. (eds) Software Engineering and Formal Methods. SEFM 2014. Lecture Notes in Computer Science(), vol 8938. Springer, Cham. https://doi.org/10.1007/978-3-319-15201-1_2
Download citation
DOI: https://doi.org/10.1007/978-3-319-15201-1_2
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-15200-4
Online ISBN: 978-3-319-15201-1
eBook Packages: Computer ScienceComputer Science (R0)