|
| 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: wsindd@win.tue.nl , robg@win.tue.nl |
| ~ |
| (2) Philips Research Labs. |
| Prof. Holstlaan 4 |
| 5656 AA Eindhoven, The Netherlands |
| Tel: +31 40 274 2953 |
| E-mail: feijs@natlab.research.philips.com |
| ~ |
| (3) Dept. of Comp. Science |
| Leiden Univ. |
| PO Box 9512 |
| 2300 RA Leiden, The Netherlands |
| E-mail: 106406.1504@compuserve.com |
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 : http://www.win.tue.nl/cs/fm/Dennis.Dams , http://www.win.tue.nl/cs/fm/Rob.Gerth , http://www.win.tue.nl/cs/fm/Loe.Feijs
This Page was prepared by Mark Jorgensen.
Back to the VASY Home page