Computing technology pervades our daily lives. It is present in devices we wear, use and rely on for work and leisure. The services these technologies provide are increasingly the result of interactions and collaborations between many devices widely distributed across a multitude of ad-hoc, dynamically changing networks. This pervasive behaviour must be captured within the specifications of the devices and networks if they are to work as intended. Otherwise flawed designs could be implemented and deployed with potentially catastrophic results. Hence it is vital to have analytical modelling techniques that uncover pertinent behaviour directly from the specifications themselves. It is equally important to have methodologies that use the analysis results obtained from the models to enhance and correct the specifications.