Abstract
CSP ∥ B is an approach to combining the process algebra CSP with the formal development method B, enabling the formal description of systems involving both event-oriented and state-oriented aspects of behaviour. The approach provides architectures which enable the application of CSP verification tools and B verification tools to the appropriate parts of the overall description. Previous work has considered how large descriptions can be verified using coarse grained component parts. This paper presents a generalisation of that work so that CSP ∥ B descriptions can be decomposed into finer grained components, chunks, which focus on demonstrating the absence of particular divergent behaviour separately. The theory underpinning chunks is applicable not only to CSP ∥ B specification but to CSP specifications. This makes it an attractive technique to decomposing large systems for analysing with FDR.
This is a preview of subscription content, log in via an institution to check access.
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)
Arbab, F.: Reo: A channel-based coordination model for component composition. Mathematical Structures in Computer Science (14), 329–366 (2004)
Butler, M.J.: csp2B: A Practical Approach to Combining CSP and B. Formal Aspects of Computing 12 (2000)
Butler, M., Leuschel, M.: Combining CSP and B for Specification and Property Verification. In: Fitzgerald, J.S., Hayes, I.J., Tarlecki, A. (eds.) FM 2005. LNCS, vol. 3582, pp. 221–236. Springer, Heidelberg (2005)
Cavalcanti, A., Sampaio, A., Woodcock, J.: Refinement of Actions in Circus. In: REFINE 2002, FME Workshop, Copenhagen (2002)
Evans, N., Treharne, H.: Investigating a File Transfer Protocol Using CSP and B. SoSym Journal (accepted for publication 2005)
Evans, N., Treharne, H., Laleau, R., Frappier, M.: How to Verify Dynamic Properties of Information Systems. In: 2nd International Conference on Software Engineering and Formal Methods. IEEE, China (2004)
Formal Systems (Europe) Ltd.: Failures-Divergences Refinement: FDR2 User Manual (1997)
Hoare, C.A.R.: Communicating Sequential Processes. Prentice Hall, Englewood Cliffs (1985)
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.A.: Concurrent and Real-Time Systems: the CSP Approach. John Wiley, Chichester (1999)
Schneider, S., Treharne, H.: Communicating B Machines. In: Bert, D., Bowen, J.P., Henson, M.C., Robinson, K. (eds.) B 2002 and ZB 2002. LNCS, vol. 2272, p. 416. Springer, Heidelberg (2002)
Schneider, S., Treharne, H.: CSP Theorems for Communicating B Machines. In: Boiten, E.A., Derrick, J., Smith, G.P. (eds.) IFM 2004. LNCS, vol. 2999. Springer, Heidelberg (2004)
Treharne, H., Schneider, S.: Using a Process Algebra to control B OPERATIONS. In: Araki, K., Galloway, A., Taguchi, K. (eds.) IFM 1999, York, pp. 437–456 (1999)
Treharne, H., Schneider, S., Bramble, M.: Composing Specifications using Communication. In: Bert, D., Bowen, J.P., King, S. (eds.) ZB 2003. LNCS, vol. 2651, pp. 58–78. Springer, Heidelberg (2003)
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
Schneider, S., Treharne, H., Evans, N. (2005). Chunks: Component Verification in CSP ∥ B. In: Romijn, J., Smith, G., van de Pol, J. (eds) Integrated Formal Methods. IFM 2005. Lecture Notes in Computer Science, vol 3771. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11589976_7
Download citation
DOI: https://doi.org/10.1007/11589976_7
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-30492-0
Online ISBN: 978-3-540-32240-5
eBook Packages: Computer ScienceComputer Science (R0)Springer Nature Proceedings Computer Science