Next: 3 Comparison
Up: 2 Position
Previous: 2.6 Validation of Formal
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.
Peter Henderson