Abstract
Formal methods are mathematically based languages for producing verifiable, consistent and more reliable formal specifications which leads to the construction of trustworthy and maintainable computer programs. Most formal methods can be classified as state-based or event-based formal methods. State-based formal methods, such as the B-Method, are capable of describing data aspects of the system but they are not able to describe behavioural aspects or concurrency. On the other hand, by using event-based formal methods, such as CSP, we are not able to describe data aspects of the system which results in difficulty to describe systems which contain state transitions. Over the years, the idea of combining state and event based formal methods has been proposed in order to design systems in which both data and behavioural aspects are described. The idea of creating a combination of state and event based formal methods which is able to describe mobility and dynamic patterns has also been raised in formal method integration. This additional functionality is suitable for modelling agent systems or peer-to-peer networks where consideration of mobility is important. CSP || B is a combination of CSP and B in which CSP processes are used as control executives for B machines. This architecture enables a B machine and its controller to interact and communicate with each other while working in parallel. The architecture has focused on sequential CSP processes as dedicated controllers for B machines. This thesis introduces Mobile CSP || B, a formal framework based on CSP || B which enables us to specify and verify concurrent systems with mobile architecture as well as the previous static architecture. In Mobile CSP || B, a parallel combination of CSP processes act as the controller for the B machines and these B machines can be transferred between CSP processes during the system execution.