MURAL - Maynooth University Research Archive Library

    A Specification of TCP/IP using Mixed Intuitionistic Linear Logic

    Gray, David and Hamilton, Geoff and Power, James F. and Sinclair, David (2001) A Specification of TCP/IP using Mixed Intuitionistic Linear Logic. In: 2nd Joint Workshop on Formal Specification of Computer-Based Systems, 20 April 2001, Washington DC, USA.

    Download (124kB) | Preview

    Share your research

    Twitter Facebook LinkedIn GooglePlus Email more...

    Add this article to your Mendeley library


    This paper presents an outline specification of the IP and TCP communication protocols in mixed intuitionistic linear logic and describes how this logic can be used to prove some properties of both protocols. We have previously presented a specification of IP in [8] using commutative linear logic; in this paper we extend this specification considerably to include TCP, which, in turn, necessitates the use of non-commutative operators. Linear logic is particularly suited to the description of state-based systems, and communication protocols in particular, since it keeps track of the resources used in each deduction step. Mixed intuitionistic linear logic is variant of linear logic that contains both commutative and non-commutative operators, and as such is useful where the order of the consumption of resources must be specified. In the following sections we brie y describe IP and TCP and linear logic. We then present an outline of our specification of the user interfaces for IP and TCP, demonstrating the role of the linear operators in the axioms. Finally, we outline the remainder of our work concerning the description of the TCP protocol itself and the verification process undertaken.

    Item Type: Conference or Workshop Item (Paper)
    Additional Information: This is an Extended Abstract of the paper presented.
    Keywords: specification; TCP; IP; mixed intuitionistic linear logic; non-commutative operators;
    Academic Unit: Faculty of Science and Engineering > Computer Science
    Item ID: 6451
    Depositing User: Dr. James Power
    Date Deposited: 07 Oct 2015 16:18
    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