- Prof. William Knottenbelt
- Prof. John Darlington
- Dr Jeremy Bradley
- Dr Tamas Suto
- Dr Harini Kulatunga
- EPSRC project EP/D505933/1
- Started in November 2005
- Completed in November 2008
- Funded value
We are surrounded by complex distributed systems such as mobile phone networks, stock market trading platforms and health care systems. When designing these systems, it is important to ensure that their performance will satisfy certain quality of service constraints. For example, in the UK, it is a government target that Accident and Emergency units see, treat and discharge 90% of patients in under four hours. Predicting distributed system performance is notoriously difficult, however, since subtle interactions between components can have large, unforeseen and detrimental effects on performance. It is therefore important to use formal frameworks which can either rigorously guarantee that performance requirements will be met, or, if not, show which suspect interactions and bottlenecks need to be addressed. The formal framework we propose is an extended continuous stochastic logic (eCSL). Although this and related logics enable the rigorous, verfiable, expressive and composable specification of performance constraints, they are not widely used by system designers in industry. There are three main reasons for this:
- It is challenging for most system designers to understand and formulate logical queries. We address this issue through the use of novel graphical model-level specification techniques. Graphical queries are then automatically translated into eCSL formulae. No understanding of the underlying logical framework is required by the system designer.
- Even if a system designer is currently able to formulate a stochastic logic query, this must be broken down and translated into the interface language of existing analysis tools manually, requiring further specialist knowledge. This problem is addressed by developing novel techniques for the automated decomposition and mapping of stochastic logic formulae into the interface languages of existing performance analysis tools.
- The solution capacity of current tools is limited, which prevents the analysis of many large-scale industrial systems. We address this problem by developing distributed and parallel analysis techniques and by exploiting the computational capacity provided by Grid systems. All our tools will be Grid-enabled and we will develop an eCSL-aware Grid execution scheduler. In this way, system designers will have access to a large pool of virtualised computing resources on tap.
This is a joint project with John Darlington. With GRAIL, we will install the AESOP computational cluster - a 64 processor, Inifiniband interconnect, cluster computer which will tackle very large computational problems as specified in performance logics such as CSL and eCSL.