DocumentCode
2332068
Title
Verification of the fast reservation protocol with delayed transmission using the tool KRONOS
Author
Tripakis, Stavros ; Yovine, Sergio
Author_Institution
VERIMAG, Gieres, France
fYear
1998
fDate
3-5 Jun 1998
Firstpage
165
Lastpage
170
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;
fLanguage
English
Publisher
ieee
Conference_Titel
Real-Time Technology and Applications Symposium, 1998. Proceedings. Fourth IEEE
Conference_Location
Denver, CO
Print_ISBN
0-8186-8569-7
Type
conf
DOI
10.1109/RTTAS.1998.683200
Filename
683200
Link To Document