Akademska digitalna zbirka SLovenije - logo
VSE knjižnice (vzajemna bibliografsko-kataložna baza podatkov COBIB.SI)
  • Exploring properties of a bounded retransmission protocol with VIS
    Meolic, Robert ; Kapus, Tatjana ; Brezočnik, Zmago
    It is of great interest for users of communications protocols to have a proof that they are correct and reliable to use. In order to prove a protocol correct formally, the protocol and the required ... properties must be formally described. This paper reports on verifying properties of a bounded retransmission protocol for large data packets. It is used to transfer files via a lossy communication channel. We emphasize timing properties of the protocol in Verilog and stated properties in a computer tree logic. The verification was carried out automatically by model checking. We used the non-commercial tool VIS which made it possible to introduce nondeterministic choice of data packets lenght and a realistic notion of time.
    Vrsta gradiva - članek, sestavni del
    Leto - 1999
    Jezik - angleški
    COBISS.SI-ID - 5341206