next up previous Final Report of the COST-247 Action

Understanding and Modelling the USB Hub

Dennis Dams(1), Rob Gerth(1), Loe Feijs(2), Gertjan Kamsteeg(3)

(1) Dept. of Math. & Comp. Science
Eindhoven Univ. of Technology
PO Box 513
5600 MB Eindhoven, The Netherlands
Tel: +31 40 247 5159/4389/4124
Fax: +31 40 246 3992
E-mail: ,
(2) Philips Research Labs.
Prof. Holstlaan 4
5656 AA Eindhoven, The Netherlands
Tel: +31 40 274 2953
(3) Dept. of Comp. Science
Leiden Univ.
PO Box 9512
2300 RA Leiden, The Netherlands


This paper describes our ongoing experiences during the a-posteriori formalisation of the USB hub protocol in Promela, and subsequent simulation and verification experiments. Such an activity forces one to consider all chosen aspects with equal (and great) precision. The paper focusses on the technical aspects of the model, the choices we had to make, and the problems we encountered. Many unclarities, inconsistencies and errors in the original text of the specification were uncovered.

This presentation has been given during the COST-247 2nd International Workshop on Applied Formal Methods in System Design (Zagreb, Croatia, June 18-19, 1997).

COST-247 Working Group(s):

Web Links : , ,

This Page was prepared by Mark Jorgensen.

Back to the VASY Home page