2.6 Validation of Formal Models

We have build a simple tool based on the operational semantics for the pi-calculus given by Milner in [Mil91]. This tool does nothing more than code up the reduction rules given in that paper, but it does it in the context of a language which can support recursion equations. The tool can be used to code up the models of the earlier sections and to then navigate through them a step at a time. A menu is provided on which each of the possible next events is listed. The experimenter chooses an event (always of the form: send a particular message on a particular channel) and the executing model then changes state, which is reflected in a change in the choices available on the menu. The experimenter can always step backwards through the execution and make an alternative choice of event, as often as necessary to conduct a manual search of the state-space.

We have also automated this state-space search where the tool constructs a finite part of the state-space and presents it in the form of a finite state machine (ie state-event-state triples). The state-space search is pruned in various ways and we are experimenting with methods of pruning such as those pioneered in the model checking tools described by Clarke [Cla91], Ip and Dill [Ip96] and Jackson [Jac96].