Sinclair, David and Power, James F. (2005) Specifying and Verifying Communications Protocols using Mixed Intuitionistic Linear Logic. Electronic Notes in Theoretical Computer Science, 133. pp. 255-273. ISSN 1571-0661

Preview

Download (241kB) | Preview

Abstract

In this paper we present a technique for specifying and verifying communications protocols and demonstrate this approach by specifying and verifying two of the fundamental communications protocols, namely TCP and IP, which form the basis of many distributed systems. The logical formalism used is Mixed Intuitionistic Linear Logic in order to use both commutative and non-commutative operators to model the concurrent and sequential processes in these protocols. Key properties of both protocols are proved.

Item Type:	Article
Additional Information:	Published under a Creative Commons license. Attribution-NonCommercial-NoDerivs 3.0 Unported (CC BY-NC-ND 3.0)
Keywords:	complex systems; formal methods; mixed intuitionistic linear logic;
Academic Unit:	Faculty of Science and Engineering > Computer Science
Item ID:	8229
Identification Number:	https://doi.org/10.1016/j.entcs.2004.08.068
Depositing User:	Dr. James Power
Date Deposited:	18 May 2017 16:07
Journal or Publication Title:	Electronic Notes in Theoretical Computer Science
Publisher:	Elsevier
Refereed:	Yes
URI:	http://www.sciencedirect.com
Use Licence:	This item is available under a Creative Commons Attribution Non Commercial Share Alike Licence (CC BY-NC-SA). Details of this licence are available here

Repository Staff Only(login required)

Item control page

Downloads

Origin of downloads