Verifying the CPA Networking Stack using SPIN/Promela.

Chalmers, Kevin; Kerridge, Jon

Verifying the CPA Networking Stack using SPIN/Promela.

Chalmers, Kevin; Kerridge, Jon

Authors

Kevin Chalmers

Jon Kerridge

Contributors

Peter H Welch
Editor

Frederick R M Barnes
Editor

Jan F Broenink
Editor

Kevin Chalmers k.chalmers@napier.ac.uk
Editor

Jan B�kgaard Pedersen
Editor

Adam T Sampson
Editor

Abstract

This paper presents a verification of the CPA Networking Stack, using the SPIN Model Checker. Our work shows that the system developed for general networking within CPA applications works under the conditions defined for it. The model itself focuses on ensuring deadlock freedom, and work still needs to be undertaken to verify expected behaviour of the architecture.

Citation

Chalmers, K., & Kerridge, J. (2013). Verifying the CPA Networking Stack using SPIN/Promela. In P. H. Welch, F. R. M. Barnes, J. F. Broenink, K. Chalmers, J. B. Pedersen, & A. T. Sampson (Eds.), Communicating Process Architectures 2013 (39-56)

Conference Name	35th WoTUG conference on concurrent and parallel programming
Start Date	Aug 25, 2013
End Date	Aug 28, 2013
Publication Date	2013
Deposit Date	Nov 27, 2014
Peer Reviewed	Peer Reviewed
Pages	39-56
Book Title	Communicating Process Architectures 2013
ISBN	978-0-9565409-7-3
Keywords	distributed systems; model checking;
Public URL	http://researchrepository.napier.ac.uk/id/eprint/7339