Title :
Verification of the fast reservation protocol with delayed transmission using the tool KRONOS
Author :
Tripakis, Stavros ; Yovine, Sergio
Author_Institution :
VERIMAG, Gieres, France
Abstract :
The authors report the work carried out at VERIMAG within the framework of an research cooperation with CNET. The goal of the work was twofold: to formally specify the FRP-DT using the timed-automaton formalism, and to analyze its behavior using the tool KRONOS. The 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
Keywords :
automata theory; formal specification; formal verification; protocols; real-time systems; CNET; FRP-DT; KRONOS tool; VERIMAG; bandwidth inconsistency; connection path; delayed transmission; fast reservation protocol; formal specification; timed-automaton formalism; timeout; verification; Asynchronous transfer mode; Bandwidth; Control systems; Delay; Embedded software; Equations; Fiber reinforced plastics; Formal specifications; Protocols; Virtual colonoscopy;
Conference_Titel :
Real-Time Technology and Applications Symposium, 1998. Proceedings. Fourth IEEE
Conference_Location :
Denver, CO
Print_ISBN :
0-8186-8569-7
DOI :
10.1109/RTTAS.1998.683200
