next up previous

Final Report of the COST-247 Action

Verification of the XTP Closing Procedure using a TLA

Tatjana Kapus, Zmago Brezocnik

Faculty of Electrical Engineering and Computer Science
University of Maribor
Smetanova ul. 17, SI-2000 Maribor, Slovenia
Email: ,
Tel: +386 62 221-112
Fax: +386 62 225-013


We give a brief presentation of a precise modular design specification of the most important aspects of the closing procedure of the Xpress Transfer Protocol (XTP Protocol Definition, Revision 3.6) written in a temporal logic of actions. We then show how some required safety and liveness properties regarding both graceful and ungraceful closing of XTP data streams can be proved using axioms and special program proof rules of the logic.

This presentation has been given during the COST-247 4th Management Committee Meeting (Berlin, Germany, February 9--10, 1995).

COST-247 Working Group(s): 2

This Page was prepared by Mark Jorgensen.

Back to the VASY Home page