Verifying the CPA Networking Stack using SPIN/Promela.

Research Output

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.

Date:

31 December 2013
Publication Status:

Published
Publisher

Open Channel Publishing Ltd.
Library of Congress:

QA75 Electronic computers. Computer science
Dewey Decimal Classification:

004 Data processing & computer science

http://researchrepository.napier.ac.uk/output/185196 <p>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.), <i>Communicating Process Architectures 2013</i>, (39-56)</p>

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)