|
| 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: kapus@uni-mb.si , brezocnik@uni-mb.si |
| 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