Using CSP to model the synchronisation process of variable length codes

Variable length codes (VLC) have found widespread use for efficient encoding of symbols with unequal probabilities in many practical situations. However, bit errors can cause a loss of decoder synchronism that often leads to error propagation. Recent advances in the development of VLC that limit the effect of error propagation, such as reversible VLC and self-synchronising VLC, contribute further to their popularity. However, it is still important to model the performance of various VLC code sets so that comparisons can be made between different coding schemes and for different applications. Communicating sequential processes (CSP) is a well-established formal description technique that allows one to analyse the behaviour of concurrently evolving processes. It has been successfully applied to industrial-scale problems. The paper describes how CSP can be applied to the modelling of the resync process of VLC. This approach offers three main advantages. First, a complete model comprises processes and events as basic building blocks, making this approach highly scalable. Second, different semantic models provide different level of abstraction. Third, tools are available for automatic generation of sync sequences, which also provide a measure of sync performance. This facilitates comparisons of different VLC schemes in addition to code sets obtained using a given coding scheme.