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

    [img]
    Preview
    Download (241kB) | Preview


    Share your research

    Twitter Facebook LinkedIn GooglePlus Email more...



    Add this article to your Mendeley library


    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:

    Repository Staff Only(login required)

    View Item Item control page

    Downloads

    Downloads per month over past year