Abstract
Specifications and implementations of systems need to be concerned with the interactions that can occur within a system and model the data structures appropriately. We are interested in combinations of formal methods which consider the state and dynamic requirements of a system. We recognise that many such combinations already exist, including, CSP || B and Circus, but we are concerned with a state description, being accessed and updated by control components with dynamically reconfigurable interconnections. Our work is motivated by what we see in Peer-to-Peer networks and Object-Oriented systems where instantiation and dynamically reconfigurable interconnection are essential paradigms. For example, in a Peer-to-Peer network nodes can act as both server and client in exchanging data to complete a certain task. Nodes are also independent and can leave or join the network at any time. In Object-Oriented systems, an object instance can be created with a unique reference. This reference can be used by other objects to communicate with the object. Our aim is to provide a formal framework which supports this kind of interaction so that the integrity of each active object or node is preserved, and so that we can reason about the overall behaviour of the system. The approach we consider in this thesis is a combination of the pi-calculus and the B-Method. In order to be able to reason about specifications based on both these notations we need common semantics. We define an approach which enables the interpretation of a B machine as a pi-calculus labelled transition system. This allows the integration of machines into parallel combination with pi-agents. As a result, this work extends B machines with instantiation and pi-calculus dynamic reconfiguration capabilities. We use a behavioural type-system with variant types to maintain low level server/client style consistencies between instances of machines and pi-process agents. (For example, all agents call operations that relate to some machine in the specification.) Using the type system, we identify a class of pi-agents whose behaviour with respect to the machine instances allows a weakest pre-condition style proof to be carried out on the agents. We use this property to define an approach for detecting agents that might cause a machine instance to diverge.