No description available.

No description available.

No description available.

No description available.

The Petri Box Calculus (PBC) consists of an algebra of box expressions, and a corresponding algebra of boxes (a class of labelled Petri nets). A compo- sitional semantics provides a translation from box expressions to boxes. The synthesis problem is to provide an algorithmic translation from boxes to box expressions. The axiomatisation problem is to provide a sound and complete axiomatisation for the fragment of the calculus under consideration, which captures a particular notion of equivalence for boxes. There are several alternative ways of defining an equivalence notion for boxes, the strongest one being net isomorphism. In this thesis, the synthesis and axiomatisation problems are investigated for net semantic isomorphism, and a slightly weaker notion of equivalence, called duplication equivalence, which can still be argued to capture a very close structural similarity of con- current systems the boxes are supposed to represent. In this thesis, a structured approach to developing a synthesis algorithm is proposed, and it is shown how this may be used to provide a framework for the production of a sound and complete axiomatisation. This method is used for several different fragments of the Petri Box Calculus, and for gener- ating axiomatisations for both isomorphism and duplication equivalence. In addition, the algorithmic problems of checking equivalence of boxes and box expressions, and generating proofs of equivalence are considered as extensions to the synthesis algorithm.

The stochastic process algebra PEPA is a powerful modelling formalism for concurrent systems, which has enjoyed considerable success over the last decade. Such modelling can help designers by allowing aspects of a system which are not readily tested, such as protocol validity and performance, to be analysed before a system is deployed. However, model construction and analysis can be challenged by the size and complexity of large scale systems, which consist of large numbers of components and thus result in state-space explosion problems. Both structural and quantitative analysis of large scale PEPA models suffers from this problem, which has limited wider applications of the PEPA language. This thesis focuses on developing PEPA, to overcome the state-space explosion problem, and make it suitable to validate and evaluate large scale computer and communications systems, in particular a content adaption framework proposed by the Mobile VCE. In this thesis, a new representation scheme for PEPA is proposed to numerically capture the structural and timing information in a model. Through this numerical representation, we have found that there is a Place/Transition structure underlying each PEPA model. Based on this structure and the theories developed for Petri nets, some important techniques for the structural analysis of PEPA have been given. These techniques do not suffer from the state-space explosion problem. They include a new method for deriving and storing the state space and an approach to finding invariants which can be used to reason qualitatively about systems. In particular, a novel deadlock-checking algorithm has been proposed to avoid the state-space explosion problem, which can not only efficiently carry out deadlock-checking for a particular system but can tell when and how a system structure lead to deadlocks. In order to avoid the state-space explosion problem encountered in the quantitative analysis of a large scale PEPA model, a fluid approximation approach has recently been proposed, which results in a set of ordinary differential equations (ODEs) to approximate the underlying CTMC. This thesis presents an improved mapping from PEPA to ODEs based on the numerical representation scheme, which extends the class of PEPA models that can be subjected to fluid approximation. Furthermore, we have established the fundamental characteristics of the derived ODEs, such as the existence, uniqueness, boundedness and nonnegativeness of the solution. The convergence of the solution as time tends to infinity for several classes of PEPA models, has been proved under some mild conditions. For general PEPA models, the convergence is proved under a particular condition, which has been revealed to relate to some famous constants of Markov chains such as the spectral gap and the Log-Sobolev constant. This thesis has established the consistency between the fluid approximation and the underlying CTMCs for PEPA, i.e. the limit of the solution is consistent with the equilibrium probability distribution corresponding to a family of underlying density dependent CTMCs. These developments and investigations for PEPA have been applied to both qualitatively and quantitatively evaluate the large scale content adaptation system proposed by the Mobile VCE. These analyses provide an assessment of the current design and should guide the development of the system and contribute towards efficient working patterns and system optimisation.

Modelling is a powerful method for understanding complex systems, which works by simplifying them to their most essential components. The choice of the components is driven by the aspects studied. The tool chosen to perform this task will determine what can be modelled, the maximum number of components which can be represented, as well as the analyses which can be performed on the system. Performance Evaluation Process Algebra (PEPA) was initially developed to tackle computer systems issues. Nevertheless, it possesses some interesting properties which could be exploited for the study of epidemiological systems. PEPA's main advantage resides in its capacity to change scale: the assumptions and parameter values describe the behaviour of a single individual, while the resulting model provides information on the population behaviour. Additionally, stochasticity and continuous time have already proven to be useful features in epidemiology. While each of these features is already available in other tools, to find all three combined in a single tool is novel, and PEPA is proposed as a useful addition to the epidemiologist's toolbox. Moreover, an algorithm has been developed which allows converting a PEPA model into a system of Ordinary Differential Equations (ODEs). This provides access to countless additional software and theoretical analysis methods which enable the epidemiologist to gain further insight into the model. Finally, most existing tools require a deep understanding of the logic they are based on and the resulting model can be difficult to read and modify. PEPA's grammar, on the other hand, is easy to understand since it is based on few, yet powerful concepts. This makes it a very accessible formalism for any epidemiologist. The objective of this thesis is to determine precisely PEPA's ability to describe epidemiological systems, as well as extend the formalism when required. This involved modelling two systems: the bubonic plague in prairie dogs, and measles in England and Wales. These models were chosen as they exhibit a good range of typical features, allowing to thoroughly test PEPA. All features required in each of these models have been analysed in detail, and a solution has been provided for representing each of these features. While some of them could be expressed in a straightforward manner, PEPA did not provide the tools to express others. In those cases, we determined methods to approach the desired behaviour, and the limitations of said methods were carefully analysed. In the case of models with a structured population, PEPA was extended to simplify their expression and facilitate the writing process of the PEPA model. The work also required the development of an algorithm to derive ODEs adapted to the type of models encountered. Finally, the PEPAdum software was developed to assist the modeller in the generation and analysis of PEPA models, by simplifying the process of writing a PEPA model with compartments, performing the average of stochastic simulations and deriving and explicitly providing the ODEs using the Stirling Amendment.

Distributed computer systems are becoming increasingly prevalent, thanks to modern technology, and this leads to significant challenges for the software developers of these systems. In particular, in order to provide a certain service level agreement with users, the performance characteristics of the system are critical. However, developers today typically consider performance only in the later stages of development, when it may be too late to make major changes to the design. In this thesis, we propose a performance driven approach to development — based around tool support that allows developers to use performance modelling techniques, while still working at the level of program code. There are two central themes to the thesis. The first is to automatically relate performance models to program code. We define the Simple Imperative Remote Invocation Language (SIRIL), and provide a probabilistic semantics that interprets a program as a Markov chain. To make such an interpretation both computable and efficient, we develop an abstract interpretation of the semantics, from which we can derive a Performance Evaluation Process Algebra (PEPA) model of the system. This is based around abstracting the domain of variables to truncated multivariate normal measures. The second theme of the thesis is to analyse large performance models by means of compositional abstraction. We use two abstraction techniques based on aggregation of states — abstract Markov chains, and stochastic bounds — and apply both of them compositionally to PEPA models. This allows us to model check properties in the three-valued Continuous Stochastic Logic (CSL), on abstracted models. We have implemented an extension to the Eclipse plug-in for PEPA, which provides a graphical interface for specifying which states in the model to aggregate, and for performing the model checking.

Process Algebras are a Formal Modelling methodology which are an effective tool for defining models of complex systems, particularly those involving multiple interacting processes. However, describing such a model using Process Algebras requires expertise from both the modeller and the domain expert. Finding the correct model to describe a system can be difficult. Further more, even with the correct model, parameter tuning to allow model outputs to match experimental data can also be both difficult and time consuming. Evolutionary Algorithms provide effective methods for finding solutions to optimisation problems with large and noisy search spaces. Evolutionary Algorithms have been proven to be well suited to investigating parameter fitting problems in order to match known data or desired behaviour. It is proposed that Process Algebras and Evolutionary Algorithms have complementary strengths for developing models of complex systems. Evolutionary Algorithms require a precise and accurate fitness function to score and rank solutions. Process Algebras can be incorporated into the fitness function to provide this mathematical score. Presented in this work is the Evolving Process Algebra (EPA) framework, designed for the application of Evolutionary Algorithms (specifically Genetic Algorithms and Genetic Programming optimisation techniques) to models described in Process Algebra (specifically PEPA and Bio-PEPA) with the aim of evolving fitter models. The EPA framework is demonstrated using multiple complex systems. For PEPA this includes the dining philosophers resource allocation problem, the repressilator genetic circuit, the G-protein cellular signal regulators and two epidemiological problems: HIV and the measles virus. For Bio-PEPA the problems include a biochemical reactant-product system, a generic genetic network, a variant of the G-protein system and three epidemiological problems derived from the measles virus. Also presented is the EPA Utility Assistant program; a lightweight graphical user interface. This is designed to open the full functionality and parallelisation of the EPA framework to beginner or naive users. In addition, the assistant program aids in collating and graphing after experiments are completed.

The problem of changing scale in models of a system is relevant in many different fields. In this thesis we investigate the problem in models of biological systems, particularly infectious disease spread and population dynamics. We investigate this problem using the process algebra \emph{Weighted Synchronous Calculus of Communicating Systems} (WSCCS). In WSCCS we can describe the different types of individual in a population and study the population by placing many of these individuals in parallel. We present an algorithm that allows us to rigorously derive mean field equations (MFE) describing the average change in the population. The algorithm takes into account the Markov chain semantics of WSCCS such that as the system being considered becomes larger, the approximation offered by the MFE tends towards the mean of the Markov chain. The traditional approach to developing population level equations of a system involves making assumptions about the behaviour of the entire population. Our approach means that the population level dynamics explained by the MFE are a direct consequence of the behaviour of individuals, which is more readily observed and measured than the behaviour of the population. In this way we develop MFE models of several different systems and compare the equations obtained to the traditional mathematical models of the system.