Model checking under fairness in ProB and its application to fair exchange protocols

D.M. Williams; J.E.J. Ruiter, de; W.J. Fokkink

doi:10.1007/978-3-642-32943-2_14

Model checking under fairness in ProB and its application to fair exchange protocols

D.M. Williams, J.E.J. Ruiter, de, W.J. Fokkink

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

7 Citations (Scopus)

Abstract

Motivated by Murray’s work on the limits of refinement testing for CSP, we propose the use of ProB to check liveness properties under assumptions of strong and weak event fairness, whose refinement-closures cannot generally be expressed as refinement checks for FDR. Such properties are necessary for the analysis of fair exchange protocols in CSP, which assume at least some messages are sent over a resilient channel. As the properties we check are refinement-closed, we retain CSP’s theory of refinement, enabling subsequent step-wise refinement of the CSP model. Moreover, we improve upon existing CSP models of fair exchange protocols by proposing a revised intruder model inspired by the one of Cederquist and Dashti. Our intruder model is stronger as we use a weaker fairness constraint.

Original language	English
Title of host publication	Theoretical Aspects of Computing – ICTAC 2012 : 9th International Colloquium, Bangalore, India, September 24-27, 2012. Proceedings
Editors	A. Roychoudhury, M. D’Souza
Place of Publication	Berlin
Publisher	Springer
Pages	168-182
ISBN (Print)	978-3-642-32942-5
DOIs	https://doi.org/10.1007/978-3-642-32943-2_14
Publication status	Published - 2012
Event	9th International Colloquium on Theoretical Aspects of Computing (ICTAC 2012) - Bangalore, India Duration: 24 Sept 2012 → 27 Sept 2012 Conference number: 9

Publication series

Name	Lecture Notes in Computer Science
Volume	7521
ISSN (Print)	0302-9743

Conference

Conference	9th International Colloquium on Theoretical Aspects of Computing (ICTAC 2012)
Abbreviated title	ICTAC 2012
Country/Territory	India
City	Bangalore
Period	24/09/12 → 27/09/12

Access to Document

10.1007/978-3-642-32943-2_14

Cite this

Williams, D. M., Ruiter, de, J. E. J., & Fokkink, W. J. (2012). Model checking under fairness in ProB and its application to fair exchange protocols. In A. Roychoudhury, & M. D’Souza (Eds.), Theoretical Aspects of Computing – ICTAC 2012 : 9th International Colloquium, Bangalore, India, September 24-27, 2012. Proceedings (pp. 168-182). (Lecture Notes in Computer Science; Vol. 7521). Springer. https://doi.org/10.1007/978-3-642-32943-2_14

Williams, D.M. ; Ruiter, de, J.E.J. ; Fokkink, W.J. / Model checking under fairness in ProB and its application to fair exchange protocols. Theoretical Aspects of Computing – ICTAC 2012 : 9th International Colloquium, Bangalore, India, September 24-27, 2012. Proceedings. editor / A. Roychoudhury ; M. D’Souza. Berlin : Springer, 2012. pp. 168-182 (Lecture Notes in Computer Science).

@inproceedings{0ddaa30abd3749669f94cfac03b8f5bb,

title = "Model checking under fairness in ProB and its application to fair exchange protocols",

abstract = "Motivated by Murray{\textquoteright}s work on the limits of refinement testing for CSP, we propose the use of ProB to check liveness properties under assumptions of strong and weak event fairness, whose refinement-closures cannot generally be expressed as refinement checks for FDR. Such properties are necessary for the analysis of fair exchange protocols in CSP, which assume at least some messages are sent over a resilient channel. As the properties we check are refinement-closed, we retain CSP{\textquoteright}s theory of refinement, enabling subsequent step-wise refinement of the CSP model. Moreover, we improve upon existing CSP models of fair exchange protocols by proposing a revised intruder model inspired by the one of Cederquist and Dashti. Our intruder model is stronger as we use a weaker fairness constraint.",

author = "D.M. Williams and {Ruiter, de}, J.E.J. and W.J. Fokkink",

year = "2012",

doi = "10.1007/978-3-642-32943-2_14",

language = "English",

isbn = "978-3-642-32942-5",

series = "Lecture Notes in Computer Science",

publisher = "Springer",

pages = "168--182",

editor = "A. Roychoudhury and M. D{\textquoteright}Souza",

booktitle = "Theoretical Aspects of Computing – ICTAC 2012 : 9th International Colloquium, Bangalore, India, September 24-27, 2012. Proceedings",

address = "Germany",

note = "9th International Colloquium on Theoretical Aspects of Computing (ICTAC 2012), ICTAC 2012 ; Conference date: 24-09-2012 Through 27-09-2012",

}

Williams, DM, Ruiter, de, JEJ & Fokkink, WJ 2012, Model checking under fairness in ProB and its application to fair exchange protocols. in A Roychoudhury & M D’Souza (eds), Theoretical Aspects of Computing – ICTAC 2012 : 9th International Colloquium, Bangalore, India, September 24-27, 2012. Proceedings. Lecture Notes in Computer Science, vol. 7521, Springer, Berlin, pp. 168-182, 9th International Colloquium on Theoretical Aspects of Computing (ICTAC 2012), Bangalore, India, 24/09/12. https://doi.org/10.1007/978-3-642-32943-2_14

Model checking under fairness in ProB and its application to fair exchange protocols. / Williams, D.M.; Ruiter, de, J.E.J.; Fokkink, W.J.
Theoretical Aspects of Computing – ICTAC 2012 : 9th International Colloquium, Bangalore, India, September 24-27, 2012. Proceedings. ed. / A. Roychoudhury; M. D’Souza. Berlin: Springer, 2012. p. 168-182 (Lecture Notes in Computer Science; Vol. 7521).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

TY - GEN

T1 - Model checking under fairness in ProB and its application to fair exchange protocols

AU - Williams, D.M.

AU - Ruiter, de, J.E.J.

AU - Fokkink, W.J.

N1 - Conference code: 9

PY - 2012

Y1 - 2012

N2 - Motivated by Murray’s work on the limits of refinement testing for CSP, we propose the use of ProB to check liveness properties under assumptions of strong and weak event fairness, whose refinement-closures cannot generally be expressed as refinement checks for FDR. Such properties are necessary for the analysis of fair exchange protocols in CSP, which assume at least some messages are sent over a resilient channel. As the properties we check are refinement-closed, we retain CSP’s theory of refinement, enabling subsequent step-wise refinement of the CSP model. Moreover, we improve upon existing CSP models of fair exchange protocols by proposing a revised intruder model inspired by the one of Cederquist and Dashti. Our intruder model is stronger as we use a weaker fairness constraint.

AB - Motivated by Murray’s work on the limits of refinement testing for CSP, we propose the use of ProB to check liveness properties under assumptions of strong and weak event fairness, whose refinement-closures cannot generally be expressed as refinement checks for FDR. Such properties are necessary for the analysis of fair exchange protocols in CSP, which assume at least some messages are sent over a resilient channel. As the properties we check are refinement-closed, we retain CSP’s theory of refinement, enabling subsequent step-wise refinement of the CSP model. Moreover, we improve upon existing CSP models of fair exchange protocols by proposing a revised intruder model inspired by the one of Cederquist and Dashti. Our intruder model is stronger as we use a weaker fairness constraint.

U2 - 10.1007/978-3-642-32943-2_14

DO - 10.1007/978-3-642-32943-2_14

M3 - Conference contribution

SN - 978-3-642-32942-5

T3 - Lecture Notes in Computer Science

SP - 168

EP - 182

BT - Theoretical Aspects of Computing – ICTAC 2012 : 9th International Colloquium, Bangalore, India, September 24-27, 2012. Proceedings

A2 - Roychoudhury, A.

A2 - D’Souza, M.

PB - Springer

CY - Berlin

T2 - 9th International Colloquium on Theoretical Aspects of Computing (ICTAC 2012)

Y2 - 24 September 2012 through 27 September 2012

ER -

Williams DM, Ruiter, de JEJ, Fokkink WJ. Model checking under fairness in ProB and its application to fair exchange protocols. In Roychoudhury A, D’Souza M, editors, Theoretical Aspects of Computing – ICTAC 2012 : 9th International Colloquium, Bangalore, India, September 24-27, 2012. Proceedings. Berlin: Springer. 2012. p. 168-182. (Lecture Notes in Computer Science). doi: 10.1007/978-3-642-32943-2_14

Model checking under fairness in ProB and its application to fair exchange protocols

Abstract

Publication series

Conference

Access to Document

Fingerprint

Cite this