Verification of the Fast Reservation Protocol with Delayed Transmission using the Tool Kronos

In this paper we report the work carried out at VERIMAG 1 within the framework of an research cooperation with CNET 2 . The goal of this work was twofold: to formally specify the FRP-DT using the timed-automaton formalism [1], and to analyze its behavior using the tool KRONOS [3]. This work has revealed some unexpected behaviors of the design such as a timeout that never expires, and transitions that never occur, and more important potential problems such as inconsistency in the bandwidth reserved along the connection path.

• Type: Conference
• Year: 1998
• Where: RTAS
• Authors: Stavros Tripakis, Sergio Yovine
• Keywords: Embedded Systems, Important Potential Problems, Research Cooperation, RTAS 1998, Timed-automaton Formalism