Abstract
This paper will present the formalisation stage of the development of the W DS. This formalization was achieved using CCA and was validated through simulation using ccaPL. The notation for CCA and the corresponding notation for ccaPL was presented. Moreover, this paper presented the formalised processes of each ambient as equations in CCA. Internal validation through simulation was achieved through a number of differ- ent scenarios which were designed to validate if the W DS was capable of detection and the sending and receiving of files and messages. Overall, the simulation was successful in showing that the modelling of the system had achieved the predefined requirements which included detection through signature-based and behaviour-based techniques, the W DS can now be implemented in JADE.