Protocol Validation, Standards, and Literate Programming

Prof. Michael Ferguson
Professor Emeritus
INRS-Telecommunications
University of Quebec

Email: michael@ferguson-by-bicycle.com

• 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 interworking
    
    
  
  
  
• a "formal" model of the protocol has the advantage of being precise, but is often met with the comment Ïs your model really my protocol?".
  
  
• this seminar discusses a system that is intended to convincingly relate a formal model written in Promela with the written standard.
  
  
• the system is intended to be used during, and in conjunction, with the standardisation process.
  
  

The modeling and validation of TDMA-RLP - an early success

• 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 telecommunications community
  • 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 standard.
  
  
• Even without validation tools, a formal notation is useful during standardization because it will allow informal validation via code walk-throughs.
  
  
• 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 message traces.
  
  
• 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 virtually unreadable.
  
  
• 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.
    
    
  
  
  

Literate Standardisation

• 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 process
  
  
• this is the only time when there are no impossible product deadline constraints
  
  
• the demonstration is a complete operational model of CDMA-RLP