Investigating a file transfer protocol using CSP and B

被引：0

作者：

Evans N. ^{[1
]}

Treharne H. ^{[2
]}

机构：

[1] Department of Computer Science, Royal Holloway, University of London, London

[2] Department of Computing, University of Surrey, Surrey

来源：

Software & Systems Modeling | 2005年 / 4卷 / 3期

基金：

英国工程与自然科学研究理事会;

关键词：

B; Combining formalisms; Compositional verification; CSP;

D O I：

10.1007/s10270-005-0084-3

中图分类号：

学科分类号：

摘要：

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. © Springer-Verlag 2005.

引用

页码：258 / 276

页数：18

共 26 条

[1]

Abadi M., Lamport L., Composing Specifications, ACM Transactions on Programming Languages and Systems, 15, 1, pp. 73-132, (1993)

[2]

Abrial J.R., The B Book: Assigning Programs to Meaning, (1996)

[3]

Abrial J.R., Extending B without changing it (for developing distributed systems), 1st Conference on the B Method, pp. 169-190, (1996)

[4]

Abrial J.R., Mussat L., Specification and Design of a Transmission Protocol by Successive Refinements using B, Mathematical Models in Program Development, 158, pp. 129-200, (1997)

[5]

Behm P., Desforges P., Maynadier J.M., METEOR: An Industrial Success in Formal Development, 1393, (1998)

[6]

Bolognesi T., Brinksma E., Introduction to the ISO Specification Language LOTOS, Computer Networks and ISDN Systems, 14, 1, pp. 25-29, (1998)

[7]

Bramble M., Investigating the consistency of combined specifications, (2004)

[8]

Butler M.J., csp2B: A Practical Approach to Combining CSP and B, Formal Aspects of Computing, 12, pp. 182-196, (2000)

[9]

Cavalcanti A., Sampaio A., Woodcock J., Refinement of Actions in Circus, (2002)

[10]

Evans N., Treharne H., Laleau R., Frappier M., How to Verify Dynamic Properties of Information Systems, IEEE International Conference on Software Engineering and Formal Methods, (2004)

← 1 2 3 →