Papers

In [6], van Langevelde, Romijn and Goga relate experiences with the tool Spin on Promela specifications of parts of net update for maintaining the net tree and the bus trees, respectively. The most important result is the discovery of non-termination of net update and a first attempt at the net panic procedure. The error was detected with Spin simulation in the original net update procedure, but not in subsequent fixes although these contained the same erroneous behaviour. In [8], Mooij and Wesselink use formal derivation methods [1] to construct an abstract version of the net tree part of net update. This is based on the correctness properties that must be obtained. Currently, the proofs are being checked in PVS, while a front end tool for such proofs to PVS is being developed. In [7], Mooij, Goga and Wesselink construct an alternative protocol for the net tree part of net update. The alternative is a mixture of 1394.1 and IEEE 802.1 (as described in [9,10]) functionality. The correctness is proved with techniques from [1]. In [2], Goga and Romijn investigate the feasibility of adjusting Promela specifications in order to restrict random simulations to interesting behaviour. A theoretic approach is given, and it is shown that given some sufficient conditions, the adjusted Promela code does not exhibit new behaviour nor new deadlocks. Using this approach, the non-terminating behaviour can finally be shown with Spin simulation in all erroneous versions of net update. A paper with manual proofs for the correctness of the net update and bus enumeration protocol at the implementation level is in preparation. Partial correctness has already been shown, termination still needs to be proved.