MURAL - Maynooth University Research Archive Library

    Specifying and Verifying Communications Protocols using Mixed Intuitionistic Linear Logic

    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

    Download (241kB) | Preview

    Share your research

    Twitter Facebook LinkedIn GooglePlus Email more...

    Add this article to your Mendeley library


    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:
    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
    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)

    View Item Item control page


    Downloads per month over past year

    Origin of downloads