Timing UDP: The HOL Model


The HOL Kananaskis-0 scripts for the main definitions and HOL theorems, and the resulting theory signatures:

Revision numbers and dates of the above files are listed here.

The host transition semantics

The host transition semantics in TNet_hostLTSScript.sml above has been rendered by our automatic typesetting tools, and can be viewed here as gzipped PostScript.

Return to project page