Abstract
In this paper a file transmission protocol specification is developed using the combination of two formal methods: CSP and B. The aim is to demonstrate that it is possible to integrate two well established formal methods whilst maintaining their individual advantages. We discuss how to compositionally verify the specification and ensure that it preserves some abstract properties. We also discuss how the structure of the specification follows a particular style which may be generally applicable when modelling other protocols using this combination .
Article PDF
Similar content being viewed by others
Avoid common mistakes on your manuscript.
References
Abadi M, Lamport L (1993) Composing Specifications. ACM Transactions on Programming Languages and Systems 15(1):73–132, January 1993
Abrial JR (1996) The B Book: Assigning Programs to Meaning. CUP
Abrial JR (1996) Extending B without changing it (for developing distributed systems). In: Habrias H (ed) 1st Conference on the B Method, Nantes, November 1996, pp 169–190
Abrial JR, Mussat L (1997) Specification and Design of a Transmission Protocol by Successive Refinements using B. Mathematical Models in Program Development 158:129–200. Springer, Nato ASI Series F: Computer and Systems Sciences
Behm P, Desforges P, Maynadier JM (1998) METEOR: An Industrial Success in Formal Development. B’98, Montpellier, April 1998, LNCS, vol 1393. Springer
Bolognesi T, Brinksma E (1998) Introduction to the ISO Specification Language LOTOS. Computer Networks and ISDN Systems 14(1):25–29, January 1998
Bramble M (2004) Investigating the consistency of combined specifications. MPhil thesis, Royal Holloway, University of London
Butler MJ (2000) csp2B: A Practical Approach to Combining CSP and B. Formal Aspects of Computing 12:182–196
Cavalcanti A, Sampaio A, Woodcock J (2002) Refinement of Actions in Circus. In: REFINE’02, FMEWorkshop, Copenhagen
Evans N, Treharne H, Laleau R, Frappier M (2004) How to Verify Dynamic Properties of Information Systems. In: IEEE International Conference on Software Engineering and Formal Methods, China. IEEE Computer Society Press
Havelund K, Shankar N (1996) Experiments in Theorem Proving and Model Checking. In: FME’96, Oxford, March 1996, LNCS, vol 1051. Springer
Goldberg A (1983) Smalltalk-80: The Interactive Programming Environment. Addison-Wesley Publishers
Helmink L, Selling MPA, Vaandrager FW (1994) Proofchecking a data link protocol. Technical Report CS-R9420, Centruum voor Wiskunde en Informatica (CWI), March 1994
Hoare CAR (1985) Communicating Sequential Processes. Prentice Hall
Lamport L, Schneider FB (1984) The “Hoare Logic” of CSP, and All That. ACM Transactions on Programming Languages and Systems 6(2):281–296, April 1984
Mateescu R (1996) Formal Description and Analysis of a Bounded Retransmission Protocol. INRIA Rapport de recherche 2965
Morgan CC (1990) Of wp and CSP. In: Feijen WHJ, van Gasteren AJM, Gries D, Misra J (eds) Beauty is our business: a birthday salute to Edsger W. Dijkstra. Springer
Roscoe AW (1998) The Theory and Practice of Concurrency. Prentice Hall
Schneider S, Treharne H (2002) Communicating B Machines. In: ZB2002, Grenoble, January 2002, LNCS, vol 2272, Springer
Schneider S, Treharne H (2002) CSP Theorems for Communicating B Machines. Technical Report CSD-TR-02-12, Dept. of Computer Science, Royal Holloway
Schneider SA (1999) Concurrent and Real-Time Systems: the CSP Approach. John Wiley
Fischer C (1997) CSP-OZ: A combination of Object-Z and CSP. In: Bowman H, Derrick J (eds) Formal Methods for Open Object-Based Distributed Systems (FMOODS ’97), vol 2. Chapman & Hall
Stepney S, Cooper D, Woodcock J (2000) An Electronic Purse Specification, Refinement and Proof. Oxford University Computing Laboratory, Technical Monograph PRG-126, July 2000
Treharne H (2000) Controlling Software Specifications. PhD Thesis, Royal Holloway, University of London
Treharne H, Schneider S, Bramble M (2003) Composing Specifications using Communication. In: ZB2003, Grenoble, June 2003, LNCS, vol 2651, Springer
Vissers CA, Scollo G, van Sinderen M, Brinksma E (1991) Specification Styles in Distributed Systems Design and Verification. TCS 89:179–206
Author information
Authors and Affiliations
Rights and permissions
About this article
Cite this article
Evans, N., Treharne, H. Investigating a file transfer protocol using CSP and B. Softw Syst Model 4, 258–276 (2005). https://doi.org/10.1007/s10270-005-0084-3
Published:
Issue Date:
DOI: https://doi.org/10.1007/s10270-005-0084-3