next up previous
Next: 3 Comparison Up: 2 Position Previous: 2.6 Validation of Formal

2.7 Future Work

Our interest in the pi-calculus arose out of a problem we posed in [Ber94], where we described process support systems built from communicating process components. We needed a language to formalise the models we were describing there so that we could validate them and develop an architecture or a componentology suited to the design of distributed process support systems. This remains our goal and so the next step is to design a set of process components suited to this task. The components described in this short note go some way towards that objective, but we still have lots of interesting investigations to pursue.

Another objective is to realise an implementation (in Java) of a process support system which has been designed and validated formally. To this end we already have developed Java classes which implement channels whose behaviour is exactly modelled by the pi-calculus. In a related project we have captured requirements for business process support for a particular organisation. Mapping these requirements onto a real implementation will be done informally within that project. Our plan is to show that this mapping can also be done formally, by using our formally specified process components and by validating their composition into a system using state-space search. There are, of course, major semantic issues which we need to deal with in relation to how accurately the pi-calculus models we have given (or will give) match the actual behaviour of real Web components. These issues will be dealt with as a significant part of our proposed componentology.


next up previous
Next: 3 Comparison Up: 2 Position Previous: 2.6 Validation of Formal

Peter Henderson
Sep. 12 1997