Share and Export
Share and Export
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
JP-Specifying-2005.pdf
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: | 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 |
| Related URLs: | |
| URI: | https://mural.maynoothuniversity.ie/id/eprint/8229 |
| 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
Downloads per month over past year
