Abstract
CSP ∥ B is a formal approach to specification that combines CSP and B. In this paper we present our tool that automatically translates a subset of executable UML (xUML) models into CSP ∥ B, for the purpose of verification and increased validation at the early stages of a software engineering development lifecycle. The tool is being developed for our industrial collaborators, AWE plc, in order to strengthen their software engineering process which uses xUML. As part of this process, AWE and Kennedy Carter Ltd. have built an xUML to SPARK Ada code generator, which is also employed to contribute a higher level of safety assurance at the latter stages of the lifecycle. Our tool is based on a model-text transformation strategy that uses the xUML meta-model to map to CSP and B constructs. The tool generates machine readable CSP and B; we present a simple example to demonstrate the transformation strategy, and the analysis of the resulting specification.
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.
References
Schneider, S., Treharne, H.: CSP theorems for communicating B machines. Formal Asp. Comput. 17(4), 390–422 (2005)
Mellor, S.J., Balcer, M.J.: Executable UML, A Foundation for Model-Driven Architecture. Addison-Wesley, Reading (2002)
Kolovos, D.S., Paige, R.F., Polack, F.A.C.: Epsilon development tools for Eclipse. In: Eclipse Summit (2006)
Hoare, C.A.R.: Communicating Sequential Processes. Prentice-Hall, Englewood Cliffs (1985)
Abrial, J.R.: The B-Book: Assigning Programs to Meanings. Cambridge University Press, Cambridge (1996)
Schneider, S.A., Treharne, H., Evans, N.: Chunks: Component verification in CSP ∥ B. In: Romijn, J.M.T., Smith, G.P., van de Pol, J. (eds.) IFM 2005. LNCS, vol. 3771, pp. 89–108. Springer, Heidelberg (2005)
Snook, C., Butler, M.: UML-B: Formal modeling and design aided by UML. ACM Trans. Softw. Eng. Methodol. 15(1), 92–122 (2006)
Group, T.V.T.: The Rose-VDM++ link. Technical report, CSK Systems (2008)
Wilkie, I., King, A., Clarke, M., Weaver, C., Raistrick, C., Francis, P.: UML ASL Reference Guide (ASL language level 2.5). Kennedy Carter Ltd (2003)
Object Management Group: UML 2.0 OCL Specification (2003)
Formal Systems Oxford: FDR 2.83 manual (2007)
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)
Schneider, S.: Concurrent and Real-Time Systems: the CSP Approach. Wiley, Chichester (1999)
Roscoe, A.W.: The theory and practice of concurrency. Prentice-Hall, Englewood Cliffs (1998)
Evans, N., Treharne, H., Laleau, R., Frappier, M.: Applying CSP ∥ B to information systems. Software and System Modeling 7(1), 85–102 (2008)
Treharne, H., Schneider, S., Grant, N., Evans, N., Ifill, W.: A step towards merging xUML and cspb. In: Dagstuhl workshop on Rigorous Methods for Software Construction and Analysis (to appear)
Anastasakis, K., Bordbar, B., Georg, G., Ray, I.: UML2Alloy: A challenging model transformation. In: Engels, G., Opdyke, B., Schmidt, D.C., Weil, F. (eds.) MODELS 2007. LNCS, vol. 4735, pp. 436–450. Springer, Heidelberg (2007)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Turner, E., Treharne, H., Schneider, S., Evans, N. (2008). Automatic Generation of CSP || B Skeletons from xUML Models. In: Fitzgerald, J.S., Haxthausen, A.E., Yenigun, H. (eds) Theoretical Aspects of Computing - ICTAC 2008. ICTAC 2008. Lecture Notes in Computer Science, vol 5160. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-85762-4_25
Download citation
DOI: https://doi.org/10.1007/978-3-540-85762-4_25
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-85761-7
Online ISBN: 978-3-540-85762-4
eBook Packages: Computer ScienceComputer Science (R0)