Abstract This special issue of the International Journal on Software Tools for Technology Transfer presents extended versions of four selected papers from QEST+FORMATS 2024, the first joint edition of the International Conference on Quantitative Evaluation of Systems (QEST) and the International Conference on Formal Modeling and Analysis of Timed Systems (FORMATS). The joint conference was held in Calgary, Canada, in September 2024. The papers provide a compact snapshot of current directions in quantitative evaluation and timed systems research.

In the last decade there has been a significant leap in the capability of foundation AI models, largely driven by the introduction and refinement of transformer-based machine learning architectures. The most visible consequence of this has been the explosion of interest and application of large language models such as ChatGPT. This is one exemplar of how a foundation model trained on a huge amount of data can be specialised for particular task, often by a phase of reinforcement learning with human feedback.

Byzantine fault-tolerant (BFT) state machine replication (SMR) is adopted to support blockchain consensus by tolerating arbitrarily faulty behaviours. However, the inherent complexity of BFT protocols makes existing BFT protocols hard to adapt to large-scale applications that require high scalability and performance. In this paper, we propose a BFT parallelism protocol designed to enhance its scalability by using a hierarchical multi-committee architecture. It also encompasses a cross-layer consensus operation flow to improve safety and support trusted execution environments (TEEs). Our proposed approach allows the lower bound on the number of peers to be reduced to$2f+1$. We show the value of our proposed protocol in comparison to other state-of-the-art BFT protocols through experiments and performance evaluations on a testbed built on a cloud platform. The proposed protocol demonstrates a remarkable level of scalability, capable of accommodating a growing number of peers. Additionally, it exhibits improved performance when contrasted with HotStuff and FastBFT, with approximately 100% and 200% enhancements, respectively.

Byzantine fault-tolerance (BFT) consensus is a fundamental building block of distributed systems such as blockchains. However, implementations based on classic PBFT and most linear PBFT-variants still suffer from message communication complexity, restricting the scalability and performance of BFT algorithms when serving large-scale systems with growing numbers of peers. To tackle the scalability and performance challenges, we proposeParBFT, a new Byzantine consensus parallelism scheme combining classic BFT protocols and a novel Bilevel Mixed-Integer Linear Programming (BL-MILP)-based optimisation model. The core aim of ParBFT is to improve scalability via parallel consensus while providing enhanced safety (i.e. ensuring consistent total order across all correct replicas). Another core novelty is the integration of the BL-MILP model into ParBFT. The BL-MILP allows us to compute optimal numerical decisions for parallel committees (i.e. the optimal number of committees and peer allocation for each committee) and improve consensus performance while ensuring security. Finally, we test the performance of the proposed ParBFT on Microsoft Azure Cloud systems with 20 to 300 peers and find that ParBFT can achieve significant improvement compared to the state-of-the-art protocols.

In this paper, we study an information flow security property for systems specified as terms of a quantitative Markovian process algebra, namely the Performance Evaluation Process Algebra (PEPA). We propose a quantitative extension of the Non-Interference property used to secure systems from the functional point view by assuming that the observers are able to measure also the timing properties of the system, e.g., the response time of certain actions or its throughput. We introduce the notion of Persistent Stochastic Non-Interference (PSNI) based on the idea that every state reachable by a process satisfies a basic Stochastic Non-Interference (SNI) property. The structural operational semantics of PEPA allows us to give two characterizations of PSNI: one based on a bisimulation-like equivalence relation inducing a lumping on the underlying Markov chain, and another one based on unwinding conditions which demand properties of individual actions. These two different characterizations naturally lead to efficient methods for the verification and construction of secure systems. A decision algorithm for PSNI is presented and an application of PSNI to a queueing system is discussed.

Bike sharing systems are a popular form of sustainable and affordable transport that has been introduced to cities around the world in recent years. Nevertheless, designing these systems to meet the requirements of the operators and also satisfy the demand of the users, is a complex problem. In this paper we focus on the recently introduced bike sharing system in the city of Edinburgh and use data analytics combined with formal modelling approaches to investigate the current behaviour and possible future behaviour of the system. Specifically we use a spatio-temporal logic, SSTL (the signal spatio-temporal logic), to formally characterise properties of the captured system, and through this identify potential problems as user demand grows. In order to investigate these problems further we use the CARMA modelling language and tool suite to construct a stochastic model of the system to investigate possible future scenarios, including decentralised redistribution. This model is parameterised and validated using data from the operational system.

High availability is one of the core properties of Infrastructure as a Service (IaaS) and ensures that users have anytime access to on-demand cloud services. However, significant variations of workflow and the presence of super-tasks, mean that heterogeneous workload can severely impact the availability of IaaS clouds. Although previous work has investigated global queues, VM deployment, and failure of PMs, two aspects are yet to be fully explored: one is the impact of task size and the other is the differing features across PMs such as the variable execution rate and capacity. To address these challenges we propose an attribute-based availability model of large scale IaaS developed in the formal modeling language CARMA. The size of tasks in our model can be a fixed integer value or follow the normal, uniform or log-normal distribution. Additionally, our model also provides an easy approach to investigating how to arrange the slack and normal resources in order to achieve availability levels. The two goals of our work are providing an analysis of the availability of IaaS and showing that the use of CARMA allows us to easily model complex phenomena that were not readily captured by other existing approaches.

Agent- or individual-based models which are based on a continuous-time Markov chain semantics are increasingly receiving attention in simulation. To reduce computational cost, model aggregation techniques based on Markov chain lumping can be leveraged. However, for models with nested, attributed agents, and arbitrary functions determining their dynamics it is not trivial to find a partition that satisfies the lumpability conditions. Thus, we exploit the potential of the so-called super-individual approaches where sub-populations of agents are approximated by representatives based on some criteria for similarity, and propose a round-based execution scheme to balance speed and accuracy of the simulations. For realization we use an expressive rule-based modeling and simulation framework, evaluate the performance using a fish habitat model, and discuss open questions for future research.

Developing analytical availability models for k-out-of-n:G warm standby repairable systems with many nonidentical components is tedious and error-prone, requiring specification of the generator matrix of a high dimensional Markov chain. Using the performance evaluation process algebra (PEPA) as an intermediary, this paper gives a new modeling approach for availability evaluation of such systems with r repair facilities. The components of the system are classified into n different groups that consist of statistically identical components following exponential time-to-failure and repair time distributions. A library of PEPA components and their actions are defined for system component groups, repair facilities, repair queue, and system dynamics. To capture the dependency of system states on components, a signaling mechanism is realized by actions with suitably high rates. A compilation tool is provided to automatically generate the PEPA model from a brief specification of the system, using the library components. This provides input for the PEPA analysis tool and is amenable to availability analysis. Examples are used to illustrate the proposed modeling method. Modeling with PEPA provides an efficient way to deal with availability evaluation of systems considered with many groups of repairable components.

Abstract Hybrid systems are manifest in both the natural and the engineered world, and their complex nature, mixing discrete control and continuous evolution, make it difficult to predict their behaviour. In recent years several process algebras for modelling hybrid systems have appeared in the literature, aimed at addressing this problem. These all assume that continuous variables in the system are modelled monolithically, often with differential equations embedded explicitly in the syntax of the process algebra expression. In HYPE an alternative approach is taken which offers finer-grained modelling with each flow or influence affecting a variable modelled separately. The overall behaviour then emerges as the composition of flows. In this paper we give a detailed account of the HYPE process algebra, its semantics, and its use for verification of systems. We establish both syntactic conditions (well-definedness) and operational restrictions (well-behavedness) to ensure reasonable behaviour in HYPE models. Furthermore we consider how the equivalence relation defined for HYPE relates to other relations previously proposed in the literature, demonstrating that our fine-grained approach leads to a more discriminating notion of equivalence. We present the HYPE model of a standard hybrid system example, both establishing that our approach can reproduce the previously obtained results and demonstrating how our compositional approach supports variations of the problem in a straightforward and flexible way.

In this work, we investigate a general performance evaluation framework for network selection strategies (NSSs) that are used in 3G-WLAN interworking networks. Instead of simulation, this framework is based on models of NSSs and is constructed using a stochastic process algebra, named Performance Evaluation Process Algebra (PEPA). It captures the traffic and mobility characteristics of mobile nodes in 3G-WLAN interworking networks and has a good expression of the behavior of the mobile nodes using different NSSs. Commonly used NSSs are evaluated from the perspectives of average throughput, handover rate, and network blocking probability. Results of the evaluation explore the effect of these NSSs on both mobile nodes and networks, as well as their characteristics in different mobility and traffic scenarios.

Stochastic process algebras combine a high-level system description in terms of interacting components, with a rigorous low-level mathematical model in terms of a stochastic process. These have proved to be valuable modelling formalisms, particularly in the areas of performance modelling and systems biology. However, they do suffer from the problem of state space explosion. Currently, the underlying stochastic process is generally derived via the small step operational semantics of the process algebra and relies on a syntactical representation of the states of the process. In this paper, we propose a numerical representation schema based on a counting abstraction. This automatically detects symmetries within the state space based on replicated components, and produces a compact state space. Moreover, as we demonstrate, it is amenable to other interpretations and thus other forms of computational analysis, enriching the set of qualitative and quantitative measures that can be derived from a model.

In this paper we report on progress in the use of stochastic process algebras for representing systems which contain many replications of components such as clients, servers and devices. Such systems have traditionally been difficult to analyse even when using high-level models because of the need to represent the vast range of their potential behaviour. Models of concurrent systems with many components very quickly exceed the storage capacity of computing devices even when efficient data structures are used to minimize the cost of representing each state. Here, we show how population-based models that make use of a continuous approximation of the discrete behaviour can be used to efficiently analyse the temporal behaviour of very large systems via their collective dynamics. This approach enables modellers to study problems that cannot be tackled with traditional discrete-state techniques such as continuous-time Markov chains.

Abstract Pervasive environments offer an increasing number of services to a large number of people moving within these environments, including timely information about where to go and when, and contextual information about the surrounding environment. This information may be conveyed to people through public displays or direct to a person’s mobile phone. People using these services interact with the system but they are also meeting other people and performing other activities as relevant opportunities arise. The design of such systems and the analysis of collective dynamic behaviour of people within them is a challenging problem. We present results on a novel usage of a scalable analysis technique in this context. We show the validity of an approach based on stochastic process-algebraic models by focussing on a representative example, i.e. emergency egress. The chosen case study has the advantage that detailed data is available from studies employing alternative analysis methods, making cross-methodology comparison possible. We also illustrate how realistic, context-dependent human behaviour, often observed in emergency egress, can naturally be embedded in the models, and how the effect of such behaviour on evacuation can be analysed in an efficient and scalable way. The proposed approach encompasses both the agent modelling viewpoint, as system behaviour emerges from specific (discrete) agent interaction, and the population viewpoint, when classes of homogeneous individuals are considered for a (continuous) approximation of overall system behaviour.

Reasoning about the performance of models of software systems typically entails the derivation of metrics such as throughput, utilization, and response time. If the model is a Markov chain, these are expressed as real functions of the chain, called reward models. The computational complexity of reward-based metrics is of the same order as the solution of the Markov chain, making the analysis infeasible when evaluating large-scale systems. In the context of the stochastic process algebra PEPA, the underlying continuous-time Markov chain has been shown to admit a deterministic (fluid) approximation as a solution of an ordinary differential equation, which effectively circumvents state-space explosion. This paper is concerned with approximating Markovian reward models for PEPA with fluid rewards, i.e., functions of the solution of the differential equation problem. It shows that (1) the Markovian reward models for typical metrics of performance enjoy asymptotic convergence to their fluid analogues, and that (2) via numerical tests, the approximation yields satisfactory accuracy in practice.

The exact performance analysis of large-scale software systems with discrete-state approaches is difficult because of the well-known problem of state-space explosion. This paper considers this problem with regard to the stochastic process algebra PEPA, presenting a deterministic approximation to the underlying Markov chain model based on ordinary differential equations. The accuracy of the approximation is assessed by means of a substantial case study of a distributed multithreaded application.

With the increasing diversity of content as well as user preferences, and the heterogeneity of devices and network technologies, content adaptation has been widely acknowledged as an effective strategy to deliver services and content to users in a variety of contexts. This paper presents an evaluation of the response time of large scale content adaptation systems being developed under the auspices of the Mobile VCE, using the high-level modelling formalism -performance evaluation process algebra (PEPA). The relevant factors of the system performance, including the operation speed of individual entities, loading and resource conditions of the system, are determined and analysed.

We model the probabilistic behavior of a system comprising a failure detector and a monitored crash-recovery target. We extend failure detectors to take account of failure recovery in the target system. This involves extending QoS measures to include the recovery detection speed and proportion of failures detected. We also extend estimating the parameters of the failure detector to achieve a required QoS to configuring the crash-recovery failure detector. We investigate the impact of the dependability of the monitored process on the QoS of our failure detector. Our analysis indicates that variation in the MTTF and MTTR of the monitored process can have a significant impact on the QoS of our failure detector. Our analysis is supported by simulations that validate our theoretical results.

The 10 items in this special issue focus on quantitative evaluation of computer systems.

As a resource reservation mechanism, the Resource ReSerVation Protocol (RSVP) faces a lot of challenges when applying it to the wireless and mobile networks. The interworking problems of RSVP and mobility management protocols have been extensively discussed over the last decade. As the solutions of this problem, mobility-aware RSVP schemes that integrate RSVP and micro-mobility management are becoming more and more popular. Therefore, the investigation on how much they improve the performance of the basic RSVP is necessary and useful. Instead of the traditional simulation based approaches, in this paper we introduce a formal performance evaluation formalism, named Performance Evaluation Process Algebra (PEPA), and employ it to investigate the performance of the basic RSVP and mobility-aware RSVP. Important performance metrics such as handover blocking probability and signalling cost are presented.

One of the major problems of deploying RSVP in the mobile environment is called theadvanceresourcereservationproblem. If an RSVP reservation path is reserved in advance in the subnet that a mobile node will visit, the mobile node can continue its QoS session smoothly when it hands over to that subnet. However, if too many network resources are used for advance reservation, new QoS sessions originating from that subnet will experience a higher probability of being blocked needlessly. In this paper, we propose a new advance resource reservation scheme that properly constrains the amount of advance reservations in a subnet and only allows the mobile nodes with large value of session-to-mobility ratio (SMR) to make advance reservation. We evaluate the proposed scheme and the results show that our scheme can effectively reduce both active and passive reservation blocking probabilities and achieves a better utilisation of the network resources, especially when the traffic intensity is high.

In this paper, we study and model a crash-recovery target and its failure detector's probabilistic behavior. We extend quality of service (QoS) metrics to measure the recovery detection speed and the proportion of the detected failures of a crash-recovery failure detector. Then the impact of the dependability of the crash-recovery target on the QoS bounds for such a crash-recovery failure detector is analysed by adopting general dependability metrics such as MTTF and MTTR. In addition, we analyse how to estimate the failure detector's parameters to achieve the QoS from a requirement based on Chen's NFD-S algorithm. We also demonstrate how to execute the configuration procedure of this crash-recovery failure detector. The simulations are based on the revised NFD-S algorithm with various MTTF and MTTR. The simulation results show that the dependability of a recoverable monitored target could have significant impact on the QoS of such a failure detector and match our analysis results.

To overcome the drawbacks of the mobile IPv6 protocol on handling local mobility management, IETF proposed the HMIPv6 protocol which introduces an intermediate mobility anchor point (MAP) to hide the movement of a mobile node within a local area. However, the MAP forms a bottleneck in the network since all the traffic destined for its served nodes has to go through it. Most research on HMIPv6 focuses on protocol optimisation, and performance analysis of HMIPv6 is usually simulation-based. In this paper, we employ a performance evaluation formalism named PEPA to investigate the performance tradeoffs of MAPs in HMIPv6. Performance measures such as response time and MAP utilisation are presented.

Abstract In this paper we consider two performance modelling techniques from the perspectives of model construction, generation of an underlying continuous time Markov process, and the potential for reduction in the Markov process. Such careful comparison of modelling techniques allows us to appreciate the strengths and weaknesses of different approaches, and facilitates cross-fertilization between them. In the present case we take a characteristic of one formalism, functional rates in Stochastic Automata Networks, and introduce it to the other formalism, Performance Evaluation Process Algebra. We investigate the benefits of this cross-fertilization, particularly from the perspectives of Markov process generation and reduction.

In this paper we show how high-level UML models of mobile computing applications can be analysed for classical performance measures such as throughput. The approach proceeds by compiling the UML model into a representation in the formally-defined modelling language of PEPA nets. The compilation process and subsequent performance analysis based on numerical solution of a continuous-time Markov chain is supported by a software tool, the Choreographer design platform. Choreographer interoperates with popular UML tools by reading and writing UML models in the XML Metadata Interchange format (XMI).

In grid applications the heterogeneity and potential failures of the computing infrastructure poses significant challenges to efficient scheduling. Performance models have been shown to be useful in providing predictions on which schedules can be based (N. Furmento et al., 2002) and most such techniques can also take account of failures and degraded service. However, when several alternative schedules are to be compared it is vital that the analysis of the models does not become so costly as to outweigh the potential gain of choosing the best schedule. Moreover, it is vital that the modelling approach can scale to match the size and complexity of realistic applications. In this paper, we present a novel method of modelling job execution on grid compute clusters. As previously we use performance evaluation process algebra (PEPA) (J. Hillston, 1996) as the system description formalism, capturing both workload and computing fabric. The novel feature is that we make a continuous approximation of the state space underlying the PEPA model and represent it as a set of ordinary differential equations (ODEs) for solution, rather than a continuous time, but discrete state space, Markov chain.

In the 1980s process algebras became widely accepted formalisms for describing and analysing concurrency. Extensions of the formalisms, incorporating some aspects of systems which had previously been abstracted, were developed for a number of different purposes. In the area of performance analysis models must quantify both timing and probability. Addressing this domain led to the formulation of stochastic process algebras. In this paper we give a brief overview of stochastic process algebras and the problems which motivated them, before focussing on their relationship with the underlying mathematical stochastic process. This is presented in the context of the PEPA formalism.

Any scheduling scheme for grid applications must make implicit or explicit assumptions about both the future behaviour of the application and the future availability and performance of grid resources. This paper describes an approach in which the future application behaviour is constrained by the use of algorithmic skeletons, facilitating modelling with a performance oriented process algebra, and future grid resource performance is predicted by the Network Weather Service (NWS) tool. The concept is illustrated through a case study involving Pipeline and Deal skeletons. A tool is presented which automatically generates and solves a set of models which are parameterised with information obtained from NWS. Some numerical results and timing information on the use of the tool are provided, illustrating the efficacy of this approach.

This paper gives a summary of some of the work of the Performance Evaluation Process Algebra (PEPA) project, which was awarded the 2004 Roger Needham Award from the BCS. Centred on the PEPA modelling formalism, the project has sought to balance theory and practice. Theoretical developments have been tested and validated by application to a wide range of problems and such case studies have provided the stimulus for new directions in theory. Both aspects of the work are presented in summary as well as some current and future research topics.

Abstract The standard design of on‐line auction systems places most of the computational load on the server and its adjacent links, resulting in a bottleneck in the system. In this paper, we investigate the impact, in terms of the performance of the server and its adjacent links, of introducing active nodes into the network. The performance study of the system is done using the stochastic process algebra formalism PEPA. Copyright © 2001 John Wiley & Sons, Ltd.

Performance Evaluation Process Algebra (PEPA) is a formal language for performance modeling based on process algebra. It has previously been shown that, by using the process algebra apparatus, compact performance models can be derived which retain the essential behavioral characteristics of the modeled system. However, no efficient algorithm for this derivation was given. We present an efficient algorithm which recognizes and takes advantage of symmetries within the model and avoids unnecessary computation. The algorithm is illustrated by a multiprocessor example.

S. Gilmore, J. Hillston; Process Algebras and Their Application to Performance Modelling: Proceedings of the Third Workshop on Process Algebra and Performance M

Efficient product form solution is one of the major attractions of queueing networks for performance modelling purposes. These models rely on a form of interaction between nodes in a network which allows them to be solved in isolation, since they behave as if independent up to normalisation. Markovian process algebras (MPA) extend classical process algebras with information about the duration of actions but retain their compositional structure: a system is modelled as an interaction of components. The advantages of this compositional structure for model construction and model simplification have already been demonstrated. In this paper we exploit results from queueing networks to identify a restricted form of interaction between suitable MPA components which leads to a product form solution. Each component of the model may be solved separately and the compositional structure of an MPA consequently facilitates efficient solution for successively more complex models. This work uses the notion of quasi-reversibility in a Markov process setting to define the type of interaction between MPA components. This leads to a substantial class of MPA definitions that have product-form solutions which is more general than the usual queueing network-based class of Markov processes.

Many modern computer and communication systems result in large, complex performance models. The compositional approach offered by stochastic process algebra constructs a model from submodels which are smaller and more easily understood. This gives the model a clear component-based structure. In this paper we present cases when this structure may be used to inform the solution of the model, leading to an efficient solution based on a decomposition of the underlying Markov process. The decomposition which we consider is time scale decomposition, based on Courtois's near complete decomposability. This work has been influenced by related work on stochastic Petri nets: we will discuss the advantages and disadvantages of taking such an approach to the development of techniques for stochastic process algebras. Our technique is illustrated by an example based on a closed network of queues with finite capacity in which blocking may occur.