New approach for protocol synthesis based on LOTOS

Bhed Bahadur Bista, Zixue Cheng, Atsushi Togashi, Norio Shiratori

    Research output: Contribution to journalArticle

    Abstract

    In communication protocols, the behaviour of a protocol entity is related to the behaviour of another protocol entity as they communicate under sets of communication rules (protocols). Thus, it is desirable to concentrate on the design of one protocol entity and generate the corresponding protocol entity automatically. Furthermore, it is desirable that the protocol is formal, precise and unambiguous that is, it is described using FDTs (Formal Description Techniques). In this paper, we propose a protocol synthesis algorithm in which, from a LOTOS specification of a single given entity, LOTOS specification of the corresponding peer entity is generated automatically. Unlike previous works, where FSMs (Finite State Machines) were used to synthesize protocols, we use LOTOS, which is one of FDTs developed by ISO, in our proposed synthesis algorithm. We prove that the generated protocol is logical errors free, collectively represented as deadlock free, if the given entity is in certain forms which are natural in the context of communication protocols.

    Original languageEnglish
    Pages (from-to)1646-1655
    Number of pages10
    JournalIEICE Transactions on Fundamentals of Electronics, Communications and Computer Sciences
    VolumeE77-A
    Issue number10
    Publication statusPublished - 1994 Oct

    Fingerprint

    Specification languages
    Synthesis
    Network protocols
    Communication Protocol
    Specification
    Specifications
    Deadlock
    State Machine
    Finite automata

    ASJC Scopus subject areas

    • Hardware and Architecture
    • Information Systems
    • Electrical and Electronic Engineering

    Cite this

    New approach for protocol synthesis based on LOTOS. / Bista, Bhed Bahadur; Cheng, Zixue; Togashi, Atsushi; Shiratori, Norio.

    In: IEICE Transactions on Fundamentals of Electronics, Communications and Computer Sciences, Vol. E77-A, No. 10, 10.1994, p. 1646-1655.

    Research output: Contribution to journalArticle

    Bista, BB, Cheng, Z, Togashi, A & Shiratori, N 1994, 'New approach for protocol synthesis based on LOTOS', IEICE Transactions on Fundamentals of Electronics, Communications and Computer Sciences, vol. E77-A, no. 10, pp. 1646-1655.
    Bista, Bhed Bahadur ; Cheng, Zixue ; Togashi, Atsushi ; Shiratori, Norio. / New approach for protocol synthesis based on LOTOS. In: IEICE Transactions on Fundamentals of Electronics, Communications and Computer Sciences. 1994 ; Vol. E77-A, No. 10. pp. 1646-1655.
    @article{ff7d73f30e6749e0a116700aeb26a899,
    title = "New approach for protocol synthesis based on LOTOS",
    abstract = "In communication protocols, the behaviour of a protocol entity is related to the behaviour of another protocol entity as they communicate under sets of communication rules (protocols). Thus, it is desirable to concentrate on the design of one protocol entity and generate the corresponding protocol entity automatically. Furthermore, it is desirable that the protocol is formal, precise and unambiguous that is, it is described using FDTs (Formal Description Techniques). In this paper, we propose a protocol synthesis algorithm in which, from a LOTOS specification of a single given entity, LOTOS specification of the corresponding peer entity is generated automatically. Unlike previous works, where FSMs (Finite State Machines) were used to synthesize protocols, we use LOTOS, which is one of FDTs developed by ISO, in our proposed synthesis algorithm. We prove that the generated protocol is logical errors free, collectively represented as deadlock free, if the given entity is in certain forms which are natural in the context of communication protocols.",
    author = "Bista, {Bhed Bahadur} and Zixue Cheng and Atsushi Togashi and Norio Shiratori",
    year = "1994",
    month = "10",
    language = "English",
    volume = "E77-A",
    pages = "1646--1655",
    journal = "IEICE Transactions on Fundamentals of Electronics, Communications and Computer Sciences",
    issn = "0916-8508",
    publisher = "Maruzen Co., Ltd/Maruzen Kabushikikaisha",
    number = "10",

    }

    TY - JOUR

    T1 - New approach for protocol synthesis based on LOTOS

    AU - Bista, Bhed Bahadur

    AU - Cheng, Zixue

    AU - Togashi, Atsushi

    AU - Shiratori, Norio

    PY - 1994/10

    Y1 - 1994/10

    N2 - In communication protocols, the behaviour of a protocol entity is related to the behaviour of another protocol entity as they communicate under sets of communication rules (protocols). Thus, it is desirable to concentrate on the design of one protocol entity and generate the corresponding protocol entity automatically. Furthermore, it is desirable that the protocol is formal, precise and unambiguous that is, it is described using FDTs (Formal Description Techniques). In this paper, we propose a protocol synthesis algorithm in which, from a LOTOS specification of a single given entity, LOTOS specification of the corresponding peer entity is generated automatically. Unlike previous works, where FSMs (Finite State Machines) were used to synthesize protocols, we use LOTOS, which is one of FDTs developed by ISO, in our proposed synthesis algorithm. We prove that the generated protocol is logical errors free, collectively represented as deadlock free, if the given entity is in certain forms which are natural in the context of communication protocols.

    AB - In communication protocols, the behaviour of a protocol entity is related to the behaviour of another protocol entity as they communicate under sets of communication rules (protocols). Thus, it is desirable to concentrate on the design of one protocol entity and generate the corresponding protocol entity automatically. Furthermore, it is desirable that the protocol is formal, precise and unambiguous that is, it is described using FDTs (Formal Description Techniques). In this paper, we propose a protocol synthesis algorithm in which, from a LOTOS specification of a single given entity, LOTOS specification of the corresponding peer entity is generated automatically. Unlike previous works, where FSMs (Finite State Machines) were used to synthesize protocols, we use LOTOS, which is one of FDTs developed by ISO, in our proposed synthesis algorithm. We prove that the generated protocol is logical errors free, collectively represented as deadlock free, if the given entity is in certain forms which are natural in the context of communication protocols.

    UR - http://www.scopus.com/inward/record.url?scp=0028530369&partnerID=8YFLogxK

    UR - http://www.scopus.com/inward/citedby.url?scp=0028530369&partnerID=8YFLogxK

    M3 - Article

    AN - SCOPUS:0028530369

    VL - E77-A

    SP - 1646

    EP - 1655

    JO - IEICE Transactions on Fundamentals of Electronics, Communications and Computer Sciences

    JF - IEICE Transactions on Fundamentals of Electronics, Communications and Computer Sciences

    SN - 0916-8508

    IS - 10

    ER -