Low level synchronisation problems in digital systems

Abstract

We have briefly discussed a class of low level synchronisation faults which can occur in digital systems. Further we have shown the necessity of solving, or avoiding, this problem in static redundant faulttolerant systems in order that the redundancy masks faults rather than generates them.

It is generally accepted that it is desirable to use formal techniques in the development of High Integrity Systems, hence we turned out attention to the issue of formally designing systems so that they can be shown to be free from the above synchronisation problems. We outlined the difficulties of expressing such problems, and verifying their absence, in existing (and possibly any future) formal specification notations. In particular we discussed the difficulty of showing that an implicit specification of synchronisation can be refined to an explicit one, via the normal refinement paradigms.

We concluded by suggesting that an alternative paradigm is required in the formal development of High Integrity Systems. This involves a hierarchy of models, as well as a hierarchy of specifications, where the models represent generic solutions to implementation problems (such as synchronisation) which are outwith the purview of the specifications notation.

Whilst this is a novel concept which has not been validated in practice, it can be seen by analogy with the development of other critical (e.g. secure) systems, that this proposed approach warrants further study.