Skip to main content

Research Repository

Advanced Search

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

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




You might also like



Downloadable Citations