Protocol Validation, Standards, and Literate Programming
Prof. Michael Ferguson
- almost all protocol standards are written in a "natural" language,
usually a variant of English
- such documents tend to be imprecise and incomplete
- imprecision and incompleteness is only bad if it
inhibits interworking from different vendors
- it is good if it allows product differentiation and
- a "formal" model of the protocol has the advantage of being
precise, but is often met with the comment Ïs your model really my
- this seminar discusses a system that is intended to
convincingly relate a formal model written in Promela with the written
- the system is intended to be used during, and in conjunction, with the
The modeling and validation of TDMA-RLP - an early
- TDMA-RLP is a very sophisticated Datalink protocol that aims to
retransmit a message only if it is known lost.
- This protocol was written in SDL, where the SDL code was the
definitive definition of the protocol.
- In the Q931 CCITT standard that states "When there is an
ambiguity in the narrative text, the SDL diagrams in Figures A-4/Q931 through
A-6/Q931 should be used to resolve the conflict. When the text and the SDL
diagrams are in disagreement, the text should be used as the prime source."
- It was the first, and possibly only, protocol that was validated
before it was published.
- A singular success of this work was the discovery by Eric Gautier,
a student at INRS, during his master's thesis work discovered that the
unbounded transmit order number, SSN could be replaced by a FIFO
queue of messages in transmit order - this was a significant
simplification of the protocol
- SDL was the language of choice because it had currency in the
- the graphical interface was considered an important feature
- there were case tools, such as SDT, available to ensure
syntactically and semantically correct SDL
- However, it had serious shortcomings:
- SDL language constructs and lack of libraries make complex algorithm
specification very difficult. A verifiable procedural programming fragment is
needed as an addition to SDL.
- SDL discarding of messages not in the receive or save set may increase
expressivity but it increases validation effort.
The RLP1 committee used the fact that SDL implicitly consumed unknown
messages in writing its standard. This meant that it was necessary to examine
all implicitly consumed messages to determine whether it should have been
implicitly consumed, or whether it was an error.
- Configuration and other global variables need to be specified and
validated in a safe consistent way.
- it had no concept of non-determinism so it was impossible to
validate incomplete specifications
- semantic correctness meant that it was type consistent
- abstract data types and operators had to be specified in SDL/ACT1
- an incredibly painful process
- messages can only be sent to PIDs and not named
processes. This was totally unacceptable. We fixed it with an
initialisation process that gave variable names to the pid and
exported them to to the appropriate process -
- SDL is not very procedurally expressive
- Some parts of telecommunication protocol standards are most easily
described in mathematics, for example, error coding equations. A machine
processable, formal mathematical notation would be a useful addition to SDL.
- the SDL diagrams used by the committee used 1m x .75m paper
- an example of the problem:
Lessons from TDMA-RLP Standardisation
- "Formal" SDL was seen as being "tedious beyond all reason." As
a result, the committee used informal SDL text extensively and in some
ways, informal SDL.
- No single formal notation is going to adequate or appropriate for a
complete standard or system. A suite of accepted formalisms for various parts
of a standard are required.
- Any formal notation must be acceptable and credible to the users of the
- Even without validation tools, a formal notation is useful during
standardization because it will allow informal validation via code
- Validation tools for industrial use and standards support require
flexible report generators. For example, it would be useful to be able to
generate custom annotations to Message Sequence Charts for both error and good
- Graphical notation may reduce the pain of using a formal notation, and
may even be a prerequisite for its acceptance, but
it is imperative that enough information be visible at one time for meaningful
discussion. This means that single screens or ordinary paper sizes will almost
certainly be inadequate. Partitioning of large SDL process diagrams makes them
- Timeout validation is one of the more difficult parts of a
standard. Notation for specifying appropriate Timeout behavior and formally
validating such behavior in a distributed environment is needed.
- Validation during standardization is very important. This leads to
several requirements for a validation system.
- It must be possible to validate partial and incomplete specifications.
- Support is necessary for tracking of partial and incomplete versions.
- Appropriate definitions of "correctness" are required for incomplete
and partial specifications.
- the new system is a merging of Knuth's "literate programming"
methodology and the ability to hyperlink sections of text.
- the object is to have understandable sections of code and relate
them convincingly to the written standard
- the system is intended to be used during the standardisation
- this is the only time when there are no impossible product deadline
- the demonstration is a complete operational model of CDMA-RLP
File translated from
On 24 Jul 2003, 06:40.