Research in Computer Science and Informatics at the University of Portsmouth

Additional information examples: York

OtherDetails (York)
This paper challenges conventional approaches to program compilation and subsequent execution on processors. Language specific processors are proposed, which are able to interpret language statements directly. The paper gives a simple example (using the Louden's "Tiny" language), where the language processsor is built on an FPGA. The advantages of the approach are that significant code-generation effort in the compiler is removed; allows efficent implementations of application programs within embedded systems; allows much of the parallelism available in the source program to be exploited. The work has seeded further research applying the approach to the C language.
This proposes a novel real-time processor architecture combining a coarse-grained reconfigurable array structure with microprogramming, to provide a parallel array of microprogrammable execution units. Individual execution units are programmed to interpret conventional object code, or provide application specific functions. Importantly for real-time systems,the processor is predictable from a execution time perspective. Performance is achieved by parallelism and flexibility, as execution units can be reprogrammed dynamically.Results show an implementation on FPGA; and how the processor can support common real-time system language facilities (eg. interrupts, blocking) predictably.This paper was given the Best Paper award. Whitham is my PhD student.
Despite decades of work in the area of fixed priority scheduling in hard real-time systems, a means for optimal assignment of priorities when processes share resources and may block had evaded researchers. Previously, process priorities were allocated merely on process time properties (eg. deadline-monotonic or rate-monotonic), hence are non-optimal when processes share resources. Building on our previous work in the same journal, we provide an algorithm that assigns optimal process priorities. This is accompanied by a mathematical proof of its correctness and optimality. Bletsas is my PhD student.
Real-time scheduling analysis usually assumes that all application processes execute on the processor. The analysis then calculates worst-case process response times assuming process executions are interleaved on the processor under some scheduling regime. Uniquely, this paper extends such analysis to typical embedded system architectures that incorporate dedicated hardware function accelerators executing in parallel with the processor. We present mathematically proven analysis that identifies the worst-case across the entire system, together with optimal analysis that calculates process worst-case response times.The paper is one of a number we have published in this area. Bletsas is my PhD student.
This paper describes a practical application of the research group's main technology innovations in binary neural networks. Spell checking is a widely studied problem and this paper shows a method that can operate particularly quickly and accurately. The approach uses a novel approach using a Correlation Matrix Memory neural network and compares the method to that used in a number of other approaches such as that found in Word. The CMM based method is faster and more accurate than those it was compared with. The method has been sold commercially by Cybula, the Groups spin off company.
This paper formalises the laws of object-oriented programming; it is the first to extend the seminal work of Hoare on laws of programming to cater for main-stream and challenging constructs like inheritance, recursive classes, dynamic binding, visibility, and type tests and casts. Completeness and soundness are both addressed, as is the derivation of elaborate transformation rules to support modern design techniques. The work was jointly supported by a Brazilian Research Agency and the American NSF as part of a collaborative programme; in its final evaluation, the project was given the highest commendation: merit of honour.
This paper gives a strategy for algebraic refinement of centralised abstract specifications to parallel designs using a new language, Circus, which integrates existing formalisms (Z, CSP, and the refinement calculus) to support refinement of state-rich reactive systems. The approach is amenable to automation, and therefore appealing to industry. Soundness is guaranteed using a relational semantics for Circus; feasibility has been established by case studies, including industrial applications. A preliminary version of the results was published in 2002 in the premier conference on formal methods (FM), which has a typical acceptance rate of 25 to 30%.
This paper defines simulation for the language considered in (Cavalcanti 1, SCP 2004), including object-oriented constructs like inheritance, dynamic binding, and recursive classes. Soundness of simulation is proved using a weakest precondition semantics. Part of the soundness argument for the algebra in (Cavalcanti 1, SCP 2004) builds on the technique presented here, by applying it in the proof of class laws. FM is the premier conference on formal methods; that year the acceptance rate was 32%. This work is part of a collaborative project funded by the Brazilian Government and the American NSF that was awarded a merit of honour in its final evaluation.
This paper contributes to the programme of research of the unifying theories of programming (UTP) by casting a model of binary multirelations in its predicative style to allow modelling angelic nondeterminism. The UTP is a model for design languages that integrate several paradigms; angelic nondeterminism is an important addition due to its central role in refinement. Soundness is established by isomorphisms to the existing UTP theories, and by calculating definitions for programming operators. The work is being used to extend the semantics of Circus (Cavalcanti 2, FACJ 2007). The project is funded by industry; application in avionics is envisaged in five years.
One of 8 papers accepted from 43 submissions, this describes the most comprehensive (and highest level - almost all related work tests code) search based testing framework to date. It demonstrates: search-based techniques outperforming (for particular structural coverage criteria) a major commercial tool; the first-ever guided search approach generating mutant killing test data; how to attack the thorny state problem with search; and how flexible search-based subset extraction techniques facilitate integration of search-based and random generation approaches (not previously attempted). The work, carried out by Zhan and supervised by Clark, is validated by extensive experimentation. (Published on-line June 2007, for subsequent journal appearance.
This demonstrates how grossly underestimated is the cryptanalytic power of nature-inspired search. Basic perceptron problems with 600 secret bits are broken (previous bests were around 200) and all recommended sizes of Pointcheval's more difficult permuted schemes are shown insecure. The analysis timing channel and profiling the results of solving many mutant 'warped' problems to solve the original problem are significant innovations. Knudsen, one of the world's leading cryptographers, cited this paper (and two others) in his position paper to the EU STORK consortium, stating: "It is of the utmost importance that the new tools are studied extensively..." (www.stork.eu.org/papers/19b_stork_lars.pdf).
For small Boolean functions (#iinp<=8) nature-inspired techniques equal (or surpass) achievements of cryptology researchers, with demonstrations of theoretically optimal profiles of non-linearity, correlation immunity and algebraic degree. Excellent autocorrelation values are typically achieved simultaneously. Search-based change of basis to achieve higher-order correlation immunity and propagation characteristics is a significant novelty; we know of no comparable approach. Counterexamples to several theoretical conjectures are also demonstrated. Nature-inspired approaches have never previously demonstrated such human-competitive achievement in cryptographic design. Further international collaboration followed [4], with an invited tutorial at Indocrypt 2003. (Work performed entirely by Clark, with co-author advice.)
All previous optimisation approaches altered truth tables until desired properties were obtained. Ours is the first to fix the desired properties of candidate functions and seek to evolve Boolean-ness (by searching over permutations of proposed Walsh spectra, supplied by Maitra's Eurocrypt 2000 theory). Subsequent collaboration with Maitra (India) and Stanica (US) used the technique to complement their theoretical work on rotation symmetric functions (presented at Fast Software Encryption 2004). Together with [2][3] this is one of the very few search-based papers to deliver competitive results in cryptographic research - achieved by international collaboration with world-class theoreticians.
This paper (published in a conference with a 29% acceptance rate) is the first to investigate 'tempering' for improving convergence in Bayesian C&RT modelling. Bayesian C&RT techniques generate an approximation to a posterior distribution over 'classification and regression tree' (C&RT) models using Markov chain Monte Carlo. Since such distributions have many local maxima, convergence can be very slow, leading a number of researchers in this area to conclude that Bayesian C&RT is impracticable. Here we provide conclusive empirical evidence that tempering improves convergence. We are using this approach to predict bird presence/absence in collaboration with ecologists at York and Helsinki.
This paper (published in a conference with an 18% acceptance rate) presents a logic-based framework for Bayesian model averaging using informative prior distributions. Here we show how stochastic logic programs (SLPs) provide an effective language with which to express prior knowledge leading to improved empirical results within an MCMC-based approach to Bayesian inference. A theoretical MCMC convergence result is given for an important special case. This work lies at the intersection of two important trends in machine learning: Bayesian approaches using MCMC and using logic. I was invited to speak on this paper at a data mining symposium (UKDDD'07).
This paper (published in a conference with a 34% acceptance rate) presents the CLP(BN) system. This research was jointly conducted by workers at the universities of Rio de Janeiro, Wisconsin-Madison and York and has led to an extension to the YAP Prolog system available from: (http://www.cos.ufrj.br/~vitor/Yap/clpbn/). CLP(BN) integrates constraint logic programming and inference in Bayesian networks to provide a first-order 'upgrade' for Bayesian nets. The paper shows (theoretically and empirically) how inductive logic programming methods can be used to `learn' CLP(BN) models.
This paper is the first to show how to do maximum likelihood parameter estimation for "stochastic logic programs (SLPs)". The presented "Failure-Adjusted Maximisation (FAM)" algorithm is now part of the PRISM system for symbolic-statistical modelling as described in the IJCAI-05 paper "Generative modeling with failure in PRISM" (Sato et al). PRISM is developed at the Tokyo Institute of Technology. It will also be described in a forthcoming textbook by Luc De Raedt (Leuven University, Belgium). Researchers at Imperial College have also used FAM for "Multi-Class Protein Fold Prediction Using Stochastic Logic Programs" (Chen et al, 2006, submitted).
Controller Area Network is used in nearly every new car manufactured in Europe. This journal paper shows that previous analysis, used since 1994 to determine if CAN messages will meet their deadlines, is flawed. The original analysis has been widely used, as lecture material, as the basis for subsequent research, and in commercial CAN analysis tools ¿ used to analyse the networks deployed in over 20 million cars. This paper highlights the flaws in the original analysis, derives correct schedulability tests, considers the impact on deployed systems and recommends corrective actions. This paper is now the reference work on CAN schedulability analysis.
In the Automotive and Avionics industries, the advent of high performance microprocessors has recently made it cost effective to implement multiple applications on a single platform. This paper addresses the problem of scheduling such applications using a set of servers. The paper provides, for the first time, exact response time analysis for hard real-time application tasks scheduled under Periodic, Sporadic and Deferrable Servers, using fixed priority pre-emptive scheduling at both local and global levels. This work was part of the FIRST project and has lead to the subsequent EU funded FRESCOR project adopting and implementing this approach as the basis of its scheduling framework.
This paper introduces and provides schedulability analysis for the Hierarchical Stack Resource Policy (HSRP); a resource locking protocol that enables multiple applications, scheduled under servers on a single processor, to access both locally- and globally-shared mutually exclusive resources such as data buffers, communications devices, on-chip peripherals, and system calls. HSRP combines ceiling priorities to limit priority inversion and an overrun and payback mechanism to limit interference. It represents a significant advance in the techniques available for the design and development of multi-application, single processor, real-time systems. The EU funded FRESCOR project has adopted this protocol as part of its scheduling framework.
This paper will apear in the proceedings for the 28th IEEE Real-Time Systems Symposium, with a 2007 citation. A DOI is currently unavailable. Whilst priority assignmen policies such as Deadline Monotonic are known to be optimal for simple system models, in practical applications tasks are subject to additional interference from interrupts, execution overruns, cycle-stealing etc. In such cases, the most robust priority assignment is the one that tolerates the maximum amount of additional interference. This paper provides the key results on robust priority assignment, the impact of which is guidance to engineers on how best to assign priorities in commercial systems.
Often, a constraint problem becomes practicably solvable only after substantial numbers of its symmetries are removed. This paper identifies matrix symmetries as a commonly-arising pattern in constraint programs and presents and evaluates the first methods for removing these symmetries, thereby making a large class of problems practicably solvable for the first time. This paper introduced an important new topic, it is heavily cited, and the techniques it introduced are widely used in practice. The work is summarised in the recent Handbook of Constraint Programming. This work, and a couple of other simultaneous projects on symmetry in constraint programming, led to a large growth of interest in the topic and symmetry is now one of the largest subareas of constraint programming.This research was performed as part of York-held EPSRC grant N16192 (Frisch was co-PI and then PI), whose results EPSRC evaluated as "outstanding." Three of the paper's co-authors were at York at the time.
Problems naturally conceived in terms of non-Boolean variables (those that can take more than two values) are frequently solved by translating them and using a Boolean SAT-solver. This paper presents the first rigorous analysis of new and existing methods for performing this translation and the first theorem identifying conditions under which at-least-one and at-most-one clauses are needed. It generalises a popular Boolean stochastic local search solver to handle non-Boolean formulas; thorough experiments show that this yields dramatic speedups, especially as the problem's domain size increases.It provides the first model for generating random formulas that vary in domain size but are otherwise similar. Frisch's collaborators were his undergraduate project students.
This paper describes how neural networks in particular can be used to implement an important part of a text search engine. The approach combines latent semantic indexing methods within a Hierarchical Neural Network framework (based on TreeGCS hierarchical clustering neural network). The methods are able to automatically build a synonym hierarchy, that interfaces into a CMM based neural network search engine. The paper represents a novel application of neural networks to this problem. The methods have been applied in the MinerTaur search engine sold by Cybula Ltd.
An invited paper from a EPSRC Pilot project (DAME) used to launch eScience in the UK. It describes a maintenance system for Rolls-Royce aero-engines. The system allows people to search and match distributed signal data for the first time, using neural network based time series search implemented over a set of distributed compute nodes. Published in one of the main books on Grid computing. The project lead into the DTI BROADEN project (£3.5M) and then into the CARMEN project (£4.5M) for use in neuroscience. The methods are also applied train fault data with the world's largest train manufacturing companies.
This invited paper is technical description of the system in the other paper `Distributed Aircraft Engine Diagnosis. This paper describes the three main components needed to achieve distributed search using high performance search engine (AURA) and new middleware (Pattern Match Controller) and a new viewer (Signal Data Explorer). The PMC providing a new way to manage distributed search. The paper explains how this is applied to Rolls Royce engine data to detect complex events in very large datasets. The technology is being exploited as the main product of Cybula, the groups spin off company.
This was the first paper presenting a systematically generated argument for using a modern microprocessor in safety critical systems. An earlier conference paper, presented at the High Assurance Systems Engineering Symposium in 2000, provided an initial, and again the first of its kind, informally derived discussion of the certification issues for modern microprocessors. Based on the argument this paper gives a detailed assessment into the difficulty in gathering the supporting evidence needed. Both papers generated a great deal of interest, from the Federal Aviation Administration (FAA) and NASA in particular. With our agreement this paper forms a basis for CAST-20, a FAA certification guidance document, and later a Request for Proposal from Aerospace Vehicle Systems Institute (AVSI) - a cooperative of aerospace companies, Department of Defense and FAA.
Scenario-based analysis is a well-recognised techniques for assessing architectures, e.g. for their modifiability. However its use is limited as it is intended for manual application. This paper overcomes this significant limitation by being the first to show how it can be applied in an automated framework that produces allocations and schedules that are flexible to change whilst guaranteeing to meet the real-time constraints. The acceptance rate for the conference was approximately 25%. Emberson is a PhD student.
Often, a constraint problem becomes practicably solvable only after substantial numbers of its symmetries are removed. The lexicographic ordering constraint has become the most popular method for removing symmetries and is now incorporated in most (if not all) major constraint-programming systems, commercial and otherwise. This paper presents the first purpose-built algorithm for incrementally propagating lexicographic ordering constraints on finite domains. The algorithm is proved to maintain generalised arc-consistency (i.e. maximum propagation) in optimal asymptotic runtime. Alternative methods are either proven to perform less propagation and/or shown by experiments to run slower. This research was performed as part of York-held EPSRC grant N16192 (Frisch was co-PI and then PI), whose results EPSRC evaluated as "outstanding." Three of the paper's co-authors were at York at the time.
Modelling a problem for solution by constraint technology has always been considered an art practiced by experts. This paper founds a new field of research by radically suggesting that model generation can be fully automated and demonstrating feasibility via a prototype rule-based system. For input to the system, the paper proposes a new language for specifying combinatorial problems at a level of abstraction above that at which modelling decisions are made. This is the first formal language that supports combinatorial problem specifications similar to those of Garey and Johnson. Its key feature is the provision of arbitrarily-nested combinatorial objects. The paper also overcomes a major technical obstacle: designing recursive modelling rules that can deal with this nesting. Frisch's co-authors were his RA and RSs when the work began.
Shows for the first time how graphs of different node and edge structure can be succesfully matched using spectral methods. Achieved in a rigourous way by using EM algorithm to handle missing correspondences as hidden data, and using SVD to optimise resulting matrix-based cost-function. Paper cited over 50 times in ISI and and 100 times in Google-scholar. Influential on those working in graph-based methods in vision (groups in Berne, Toronto, Siena, Alberta) and statistical shape-analysis community (Mardia). EPSRC grant supporting work (Relational Models for Recognition and Learning) rated internationally leading/oustanding. Luo was RS under supervision of Hancock. Has lead to an EU INTAS project on protein structure matching with Moscow State University, BRIEM and UIIP Minsk, and University of Balearic Islands. A 4 page abstract describing a preliminary stage of this work appeared in ICPR 2000 but was not used in the previous RAE. The archival journal version appearing in PAMI 2001 describes a significantly improved algorithm and additionally gives a) an in-depth literature review, b) a detailed and rigorous theoretical development of the method commencing from a Bayesian specification of the correspondence problem, c) a detailed matrix analysis of the EM correspondence update process, and, d) a full experimental evaluation of the method including a detailed sensitivity analysis and an in-depth comparative study.
Fixed priority scheduling (FPS) is intended for use in safety-critical systems, however prior to this work industry had rarely adopted it. A detailed evaluation revealed a number of problems with the model, e.g. preemptive scheduling makes testing more difficult and most analysis doesn't allow for realistic overheads. This paper was the culmination of my PhD which overcome these problems and set the ground work for the first use of FPS on real aircraft projects, e.g. Rolls-Royce BR715, that are now in service. As such it represents a significant and novel contribution with sufficient rigour to be a basis for real certified systems.
In paper [Bate 3] new, more flexible, scheduling techniques where introduced for safety-critical systems. This however raised the issue of what are the possible timing requirements. In this paper combinations of search and scenario-based assessment with static analysis and simulation are used to determine in a rigorous manner the valid ranges of timing requirements and control properties for a given system based on a realistic computational model rather than unrealistic assumptions. It represents a novel contribution to model-based development allowing the designer to concentrate on the overall system objectives and leave the low-level design, both functional and non-functional, to automation.
This paper presents a mathematical formulation of a schedulability analysis theory of a unified process model of periodic and non-periodic task systems.This is a needed extension for accurate and efficient schedulability analysis tools. Some of the techniques developed in this paper are being used in both academic and commercial schedulability analysis tools.
This paper argues that distributions of execution times are essential in enabling the timing analysis of next generation real-time systems. It also demonstrates that it is not correct to assume independence in the statistical sense in the general case. The paper introduces a new mathematical approach based on an algebra of distributions of execution times using safe models of dependence between software components. In a later work, it has been demonstrated the equivalence of this formulation with the general statistical theory of dependency called the theory of Copulas. The mathematical formulation has been implemented and now is a key component of the commercial tool RapiTime (commercialised by the spin-off company Rapita Systems Ltd) which is being used in Avionics, Space, Telecommunication and Automotive companies. (Colin was a post-doc working with Bernat, Petters was an RA on NextTTA EU project).
Fixed priority systems are perceived as being inflexible compared to other dynamic approaches. We demonstrated through mathematical formulation and extensive experimental evaluation that the advantages of more non-deterministic scheduling algorithms can be incorporated into fixed priority systems based on the notion of a guaranteed maximum number of deadline misses and fast on-line acceptance tests. (Cayssials was a post-doc working with Bernat)
First principled attempt to recast graph-matching problem as string-matching. Achieved using techniques from spectral graph theory. String order is established using leading eigenvector of a modified Laplacian matrix, and strings are matched using edit-costs rigourously derived from Bayes model of alignment errors. Early version of work appears in ICCV 2003 (acceptance rate 23%). Idea taken further by Gori and co-workers in 2005 IEEE PAMI paper. Robles-Kelly RA/RS supervised by Hancock. Work supported by EPSRC project (Spectral Retrieval from Large Structural Databases); final report rated internationally leading/outstanding.
First paper to rigourously formulate learning a statistical model of variations in tree structure using description length principal. Theoretically establishes novel link between the entropy of tree structures and tree edit distance. Applied to learning shape-classes from skeletons of silhouettes. First author was PhD student supervised by Hancock, and supported by DERA grant. Early version of work appears in ECCV 2004 as oral paper (acceptance rate 5%). Proving influential on graph clustering community (groups at Berne, Salerno, TU Berlin) and UIUC (Ahuju) work on visual learning of texture (ICCV2007).
Paper shows for first time how polarisation information can be used to perform two-view reconstruction of featureless shaded surfaces. Early versions of work appear in ICCV 2005n(acceptance rate 20%) and as a podium presentation at CVPR 2006 (5% accaptance rate). Work has proved influential on Ikeuchi group at Tokyo U (PAMI 29/11). Work potentially points to the design of a non-invasive range scanner that can be used for untextured and structureless surfaces and for determining material reflectance properties.
A secure protocol automated design framework is presented covering almost all of BAN logic, allowing, for the first time, protocol designs to be evolved that make use of public key, symmetric key, or hybrid schemes. Of the 45 concrete protocols in the Clark-Jacob library (an acknowledged secure protocols reference corpus) 38 had specifications expressible in BAN logic and the framework was able to generate designs satisfying all of these. We know of no similar demonstration of protocol refinement power by any other authors.
Eiffel is a clean, object-oriented programming language, orginally proposed by Bertrand Meyer, which is distinguished by forcing objects of a descendent class to obey any contracts offered by an ancestor class. SCOOP is a language mechanism, also proposed by Meyer, to extend Eiffel with a concurrency mechanism. This paper examines the issues of providing a formal semantics for SCOOP, and proposes one, by modelling the appropriate parts of the language in Hoare's CSP. The semantics is animated via a purpose-built model-checker.
There has been little use of guided search to discover substitution boxes (S-boxes) with desirable cryptographic properties. S-boxes present major computational challenges for such approaches. This paper targets small (eight inputs/outputs or fewer) S-boxes. The best previous search based work (by Burnet et al.) had sought S-boxes with high non-linearity and low autocorrelation. Here we generate S-boxes that simultaneously have higher non-linearity and lower autocorrelation than the best individual properties of S-boxes obtained by Burnet et al.
This is the first demonstration that guided search can discover cryptosystem components (Boolean functions) simultaneously possessing identified cryptanalytic resilience properties and nasty trapdoor properties. Honestly sought functions are empirically shown to be discernibly different from when attempts are made to incorporate trapdoor properties. Designers trying to incorporate malicious properties can be exposed. Experiments demonstrate how trade-offs can be made between public and secret properties. This is the first paper to address the `dark side' of guided search in cryptographic design and the first to establish the potential of such techniques to be verifiably honest; claimed searches can be reproduced by doubters
This is the archival publication of two novel ideas: (1) a general methodology for making inductive logic programming (ILP) applicable to unannotated data through the use of unsupervised learning (UL) as a pre-processing step, and (2) the naïve theory of morphology (NTM), the first applicable in practice combination of search and an information-theoretic bias for the UL of word morphology. UL of language uses cheap and abundant raw text, which substantially decreases the cost of developing linguistic tools, and makes it at all possible for languages lacking annotated corpora. NTM was an important step towards large-scale practical tools, such as Linguistica 2000 (Goldsmith, Comp.Ling. 2001). The ILP tool CLOG used here was first described in (Manandhar, Dzeroski & Erjavec, ILP'98). NTM and its coupling with ILP were first presented by Kazakov and Manandhar at ILP'98. Here the idea is generalised by proposing a variety of suitable UL pre-processing steps, analysing the pros and cons of each, and comparing one (Harris's) with NTM. An original, large, hand-crafted data set was developed for that purpose. It was also used to test for the first time the parameter space of NTM and the hybrid UL+ILP learner on the word segmentation task.
This is the first study to compare the relative benefits of communication (in the form of exchange of directions to resources) with sharing in kind and with selfish exploration. The effect of four common factors is systematically explored in a multi-agent simulation, to identify the conditions under which agents would best benefit from language. An agent designer can use these results to choose the best form of cooperation. The results highlight the evolutionary pressures promoting human use of language, and discuss from an original perspective the origin of and need for the human faculty to parse context-free language (cf. Fitch&Hauser, Sci 2004).
This is the first study to uncover, through systematic simulations, the decisive effect on the evolution of cooperation of two previously unstudied factors: (1) knowledge of degree of relatedness, and (2) the choice of sharing function. The paper fills a significant gap between the neo-Darwinist studies of evolutionary stable cooperation as kin selection (Hamilton, 1964), and its computer simulations within a game-theoretical framework (Axelrod, 1984). The results can be used wherever the dynamics of cooperation plays a role, e.g., to design robust multi-agent systems, explain biological phenomena or motivate social policies, such as taxation.
This is the first study of the evolution of syntactic communication as a form of multi-agent learning which allows a population to improve its exploitation of resources. The paper formally demonstrates the algorithmic equivalence between the mechanisms behind certain forms of navigation and language. A multi-agent simulation is then used to show the viability of evolving syntax in the context of sharing directions. The paper is an important link between Steels' work on evolving shared vocabulary (Art.Life, 1995) and the recent trend of seeing the human faculty of language as sharing components with other species (Hauser, Chomsky, Fitch: Sci, 2002).
Previous work on safety justification of Artificial Neural Networks (ANNs) has relied on process-based arguments (considered weak by the safety community), external mitigation and/or prohibition of on-line learning. This paper presents a novel analytic approach that defines a product-oriented safety case and safety lifecycle made possible through transparent rule insertion and extraction, a modified FSOM (Fuzzy Self Organising Map) architecture (with inbuilt, adaptable, constraints), and constrained learning algorithms. Application of the approach to a function approximation problem 'Inlet Guide Vane Control for a Rolls-Royce aeroengine' is presented. This approach has influenced the ANN IV&V methodology produced by ISR for NASA.
The paper presents the novel application of machine learning (ML) to hazard identification for Systems of Systems (SoS). Conventional hazard analyses cannot cope with prediction of failure effects arising from non-deterministic system interactions. Our approach uses exploratory Multi-Agent System (MAS) simulations to investigate (SoS) effects of deviant system behaviour, and ML to interpret simulation results. The approach is implemented using the MASON framework and WEKA ML toolkit (specifically Quinlan's C4.5 Decision Tree Learning algorithm). The results have led to MoD funding to integrate with battlespace simulations, and have influenced the certification work within the BAE SYSTEMS / EPSRC NECTISE project.
This paper presents the first published approach to modularising safety case arguments based upon principles of architecture construction and evaluation. It presents a systematic method for managing modular safety case dependencies adapted from `design-by-contract' principles. The extensions to the Goal Structuring Notation (GSN) have been implemented in commercial tools (e.g. Adelard's ACSE). `Modular' GSN, as proposed in this paper, has been adopted by Smiths Industries (USA) for Boeing 787 Common Core System certification. The approach forms the basis for a major MoD study into modular certification performed by the Industry Avionics Working Group and has also influenced Praxis' SafSec Methodology.
To enable Artificial Neural Networks (ANNs) to be used in safety-critical applications requires transparency in their behaviour and a means of constraining adaptation within safe bounds. This paper defines a novel constrained hybrid ANN that supports (white-box) analytic certification arguments. Failure modes of the ANN are identified and rigorous safety arguments for their mitigation (based upon the constrained behaviour of the ANN) are presented. A novel learning algorithm that adheres to pre-defined safety constraints is also presented. This work has spawned further research (funded by the SEAS DTC and ESPRC LSCITS programmes) into the certification of adaptive and autonomous systems.
This article extends an earlier article "The Duality of Knowledge" (2002). The previous article highlighted the similarities between the notion of hard / soft duality developed by Kimble and Hildreth and Wenger's notion of a Participation / Reification duality. This article provides the details of the case study that formed the basis for the previous article and uses this to explore the implications for Distributed Collaborative Working and Knowledge Management, in particular: the role that shared artefacts play in sharing knowledge and facilitating participation and the importance of building and sustaining personal relationships and the role that face-to-face meetings played in this.
The article uses some of the ideas from the article "The Duality of Knowledge" to argue for a re-evaluation of the role that Knowledge Based Systems (KBS) could play in Knowledge Management (KM). KBS were once seen as the solution to many of the problems of KM, but currently they have fallen from favour due to the unrealistic expectations that were placed upon them. The original contribution of this article is in re-visiting a neglected area and throwing new light on old problems. The article highlights some of the current developments in KBS and shows how the new generation of KBS can become effective tools for managing knowledge.
This paper addresses one of the key problems for building Knowledge Based Systems - building models that can be used to develop the systems effectively. There is no standardised approach to knowledge modelling and the many of techniques that are used are ad hoc adaptations of techniques from software engineering. This paper presents the adoption of a profile mechanism for the design of knowledge-based systems based on UML using the meta-model extension approach of UML based on XMF. It is believed that the approach outlined in this paper, which builds on existing technologies and techniques, has the potential to form the basis a standardised approach to knowledge modelling.
The paper is based around the problem of closing the web usage mining "loop". It describes the design of an experiment to find the scope of the problem of lost data due to caching and/or proxy servers and uses a novel technique known as a "footstep graph" to document the results. The paper also describes and evaluates an algorithm to restore some of this missing data. The original contribution of this paper is both the use of the footstep graph and the way in which several diverse strands of research have been brought together to solve this problem.
The paper analyses for the first time parameter settings for ant colony system optimisation (ACO), adapting a statistically well-founded approach. The contributions are both a general methodology and models that can be used to predict ACO performance given parameter settings and problem characteristics. Gecco is the most important conference for evolutionary computation and artificial life, and is highly competitive. The paper has received excellent reviews and has been nominated for the best paper award: in this track four papers received a nomination (out of 59 submissions and 22 accepted papers). A related paper analysing the MMAS heuristic won the best paper award at SLS 2007.
This paper investigates the problem of distributed multi-agent exploration of unknown environments. It proposes various algorithms that are evaluated under different conditions and with varying settings (e.g. limited/no communication). The work has been carried out in collaboration with QinetiQ, in the context of their autonomous unmanned vehicle program. Amongst others, this work has led to QinetiQ/MoD grants in the unmanned vehicle and sensor planning application areas. ECAI is one of the three top international venues for Artificial Intelligence. It takes place only every two years. The acceptance rates range from 20% to 25%.
This paper presents an integrated system for automatic mediation in group decision making. Amongst the applications studied, the system enables groups of users to reach fair decisions in joint purchases (e.g., vacation packages). The research was carried out in collaboration with the DFKI in Germany, one of the world leading AI labs. The system was subsequently integrated in a large framework at the DFKI [MIAU, Baldes et al., 2003]. The User Modeling conference is the leading event for research on personalized computing. It takes place only every two years and has an acceptance rate between 20% and 25%.
This paper presented for the first time an algorithm that enables totally independent agents to converge towards optimal joint actions in two-player normal-form games. Some of the normal form games tackled in the paper were previously considered to be especially difficult to solve in an earlier landmark paper [Claus&Boutillier, 1998], even for non-independent agents. We showed that these difficult games can be solved by agents that not only don't observe each other's actions, but that even aren't aware of each other's presence. AAAI is one of the top three venues for Artificial Intelligence, and the acceptance rate is around 20%.
The paper (published in a conference with an acceptance rate of 20.7%) describes a method for combining stochastic and non-stochastic variables within a new stochastic constraint programming paradigm. The stochastic constraint programming framework is a general purpose framework that permits treating the constraint programming component as a black box and the stochastic component can be layered on top using the idea of scenarios. The paper introduces new methodology within constraint programming that so far was proved far-fetched i.e. combining the strict logical properties of constraint programs with notion of stochastic variables. This paper present the initial ideas and experiments.
The paper is a result of an ongoing collaboration with University of Rome, Tor-Vergata that extends our earlier work reported in ECIR 2007 and shows how kernel based methods can be used in Question-Answering (QA) systems. The novelty of the work lies in extending tree kernel methods to syntactic and semantic trees and their combinations thus paving the way for new research direction in applying such methods for deep linguistic processing. Such methods hold huge promise as it changes the focus from the low level feature engineering that is the hallmark of supervised learning to general purpose similarity functions.
The paper conducts an in-depth study of methods for implementing clarification dialogues in open-domain question answering systems. As part of the work, we have developed a corpus of clarification dialogues that we collected from a study done at York. A number of key researchers (such as Bonnie Webber from Edinburgh) have now requested the use of the corpora in their own work. In the first Interactive Question Answering (IQA) workshop organised by HLT-NAACL 2006 Fan Yang (Oregon), Junlan Feng and Giuseppe Di Fabbrizio (AT&T Labs) have taken our work as the starting point for using machine learning methods in identifying clarification requests.
The paper investigates in-depth a number of case studies in the application of scenario based stochastic programming to real world problems. It refines the previously developed algorithm to make it scalable to large real world problems. In doing so the paper brings together techniques from economics into stochastic constraint programming. The method allows various metrics, such as expected value, risk etc, to be maximized/minimized for a single solution or policy. As of 26 October 2006, the paper was the 2nd most viewed paper listed in the Journal of Constraints website (http://www.springer.com/west/home/computer/artificial?SGWID=4-147-70-35487134-detailsPage=journal
McDermid's work has had a significant cumulative impact on industry, especially defence and aerospace, through research, technology transfer, continuing professional development (CPD), consultancy and influencing standards. Long-running collaborations exist with Airbus, BAE Systems, QinetiQ and Rolls-Royce. Examples of technology transfer from research include: application of product line techniques to engine control and monitoring systems, e.g. the Trent 900/Trent 1000 engine monitoring unit, reducing the cost and risk of development; CPD activities are undertaken globally, e.g. for Lockheed Martin (rail) in the USA, and with the ANU in Australia; recent CPD work for the CAA is enabling process and culture change in moving to auditing against a safety management system, instead of prescriptive regulations. An example of technology transfer via consultancy is: development of the safety assessment process and safety case strategy for the M42 automated highway, enabling safe four lane running thereby increasing road throughput by about 25%, and saving of about £500M in road building costs. McDermid was one of the primary authors of Defence Standard 00-56 Issue 4 (the main defence safety standard); he is engaged in harmonising 00-56 with the US MilStd 882 (a technical and political challenge) and is influencing the reworking of the main civil aerospace safety standards, e.g. ARP 4754 This paper illustrates technology transfer from research with Rolls-Royce. Compressed timescales in the development of systems and software force the use of concurrent engineering, where requirements and design evolve in parallel. A critical problem is the potential invalidation of design commitments due to changes in requirements. The paper introduces a novel technique for analysing uncertainty in requirements, and establishing architectural flexibility requirements to counteract the uncertainty and to reduce the impact of change. The approach was validated against several issues of the Rolls-Royce Trent 500 controller specifications, and shown to be highly effective.
Formal techniques are most justified in safety critical applications, but systems engineers use tools like Matlab/Simulink/Stateflow (MSS) to produce diagrams representing control laws and moding. Gaining value from formal methods requires integration with tools such as MSS, and software methods such as UML; providing integration of control, software engineering and safety methods is novel and crucial to industrial take-up. The paper describes this integration and its use for validating specifications against derived safety requirements; it also describes a support tool (SSA) integrated into MSS. SSA is now integrated into HIS VDS toolset, which will enable its wider use.
Features of object oriented (OO) programs, e.g. polymorphism, make them difficult to test; there are several proposed OO test methods, but they had not been evaluated. The novel contribution of this paper is to provide a method for evaluating effectiveness of OO testing; the method uses a mutation approach. The paper reports application of the approach to industrial code (from IBM). The paper shows weaknesses in published methods,and how to overcome them, e.g. by adding tests for statement coverage. The paper has more than 40 Google Scholar citations.
Networked systems where data and processes are mobile bring new security challenges. Security is essentially about risk; the paper starts from fundamentals, deriving a novel method for risk-based network security analysis. This supports new forms of security requirement, e.g. restrictions on data distribution/location, and new design principles, e.g. on integrity management. The approach was validated in the EPSRC eScience DAME project, showing how to protect sensitive engine health-monitoring data, to derisk planned operational systems. The work also underpins the security elements in the $135M, 10 year ITA project on military mobile networks. (Work whilst Chivers RAEng Fellow at York.)
Originality: In this paper we construct a decision table classifier using only the binary elements of the binary correlation matrix memory with fixed weight inputs and outputs. Rigour: The approach was evaluated against an implementation of Wettscherek's attribute selection algorithm on data from the UCI repository, and found to be an order of magnitude faster for selecting significant attributes compared to the standard implementation. Significance: This is the first time that it has been demonstrated that this biologically plausible but technically simple neural network architecture can implement a powerful statistical classifier, albeit with a particular coding restriction on the input and output data.
Originality: A self-organising map is used to form a representation of real-valued input data. The regular structure of the map is used to produce the fixed weight binary codes necessary for a binary correlation matrix memory. This is not just reduction of the dimensionality of the input data, but creating an encoding using the structure of the reduced data. Rigour: The approach was evaluated by constructing classifiers for data from the UCI repository, to determine whether classification performance was maintained whilst reducing memory requirements. Significance: This is a practical coding method to make binary associative memories more memory efficient, and it shows how general purpose systems can be constructed around binary memory.
Originality: A new framework for the use of neural networks in datamining is presented. The framework outlines the behaviour required of a neural network for its use in data mining to give some gain over other methods. Rigour: The framework is used to evaluate the Self-Organising Map as a candidate network for data-mining. A SOM is used to create a representation of a database containing a synthetic dataset(with known itemset structure). The approach is able to identify clusters of associated records, and also to indicate the dependencies between them. Significance: This is an area in which little has so far been done with neural networks. The framework is not specific to any particular network architecture.
Originality: A probabilistic data-mining method is defined for extracting item-set support from a self-organising map. Self organising maps have been used in the context of data mining before, but this is the first time they have been used to generate item-set support directly. Rigour: The support for item-sets was calculated using both the standard "apriori" algorithm and the self-organising map, for four artificial data-sets and three real data-sets from a public data-mining repository, and the divergence found to be very small. Significance: The construction of the Self-organising map is independent of the item-set query and can therefore be done once, in advance. The resulting map may be used to answer any support query very quickly, unlike other algorithms which require repeated passes through the database for each query.
This paper presents the first rigorous approach to the formal refinement of abstract OO specifications to code within the context of a real programming language, Eiffel. It builds on Hehner's predicative calculus for refinement, and introduces a formal semantics for a substantial subset of Eiffel. Its novelties include theories for reasoning about pointers, aliasing, and real-time. Its ideas have been used by groups in Toronto, Macau, York, Zurich, the last in particular to help define links between Eiffel and automated provers e.g., Spec#.
This paper presents the first complete language-independent and tool-supported solution to the problem of merging arbitrary models in the context of model-driven development. EML was derived from industrial use cases within the MODELWARE European project, and was validated by project stakeholders. EML has been used by developers and researchers at Fraunhofer, IBM Haifa, WM-Data, Seville, LIP6, and INRIA to solve model management problems. It is an Eclipse GMT open-source component, with industrial and academic validation. The work was supported by MODELWARE, and received the highest rating by the project reviewers. MoDELS is the premier MDD conference, selecting 25% of submissions.
The paper makes four novel contributions: it shows how to use theorem proving technology (PVS) to analyse industrial strength standards for metamodelling, conformance, and consistency checking; it gives a novel axiomatization of models and metamodel theory; it shows how to use executable specifications to do conformance and consistency checking via simulation; and it provides a novel comparison framework and detailed analysis of the advantages and disadvantages of each approach. The work was developed MODELWARE, and was used by partners Thales, SINTEF, Fraunhofer, INRIA, and IBM. It provides a rigorous link between industrial standards for MDD, and formal techniques. The paper builds on work first presented at ETAPS'01, and the work was funded by the EU and NSERC.
This presents the first extensible domain-specific language for architectural modelling and analysis of high-integrity real-time systems. Its formal definition includes structural modelling and contracts for reliability, and contributes a design-by-views and a layered approach for building HIRTS. It is a major contribution to EPSRC DARP HIRTS, used by BAE Systems, Rolls-Royce, and QinetiQ, and is the subject of five papers. It has been validated by the DARP industrial partners, and used on three real case studies for real-time systems. The paper itself was one of six selected for the special issue on architectures, out of 44 submissions. It has influenced the AADL, SysML, and UML Profile for AADL standards currently under development.
Originality: A new and effective method of mobile robot steering control is presented, which uses an automatically generated vector field of velocity around the planned path. Rigour: mathematical modelling of the system and simulation results show the effectiveness of the technique for tracking parametric curves. Significance: The approach is suitable for any kinematic configuration and the system can manoeuvre accurately at low speeds by deriving control parameters as functions of velocity. The approach is practical, as the peak torque demand on the steering controller is reduced, using a technique which distributes steering curvature changes evenly over the extent of a manoeuvre.
Originality: A new approach for reconstructing realistic 3D models of buildings from image sequences. Contributions include (i) Highly accurate fundamental matrix estimation using homography constraints. (ii) A new rectification algorithm using epipolar geometry constraints. (iii) A self-calibration method, which uses prior knowledge of orthogonal planes (lines) and parallel lines to act as constraints on the absolute quadric. Rigour: The way in which the absolute quadric is constrained is shown with mathematical rigour. All techniques are tested on a range of real imagery. Significance: The techniques may be used for virtual reality, movie special effects, and many other graphical applications.
Originality: A new image transformation called "reciprocal-polar (RP) rectification" is presented. Under (near) pure translation, planar motion in RP-space is a pure shift along a scan line and hence can be recovered by 1D signal correlation over large motions, where all other methods fail. Rigour: We prove mathematically that, across the whole RP-image space, planar motion lies on a 3D sinusoidal manifold, thus allowing accurate segmentation, using robust sinusoidal model fitting. A large selection of both synthetic data and real imagery verified the approach. Significance: Extremely useful in any application where the segmentation and/or motion of a planar region is required. Successfully employed for robot obstacle detection, detection of obstacles on aircraft runways and visual metrology.
Originality: A new 3D face recognition method is presented. First work to apply linear discriminant analysis (LDA) to 3D facial depth maps. First work to represent 3D faces using a large variety of pixel-level surface feature maps. First work to apply LDA to these surface feature maps. Rigour: evaluated on the largest 3D dataset available at the time (1770 3D face maps, many poor quality) giving 7.2% equal error rate. Significance: patent and journal paper published, technology licensed to spin out (Cybula Ltd) and several prototype systems sold in the UK and USA. Paper submitted 24/02/2005, accepted 8/12/2005 and appeared online in final (unpaginated) form 19/12/2006.
Multimedia documents inherently use techniques that can make them accessible to people with print-related disabilities. A system was developed and evaluated which created multimedia documents to meet the needs of five print-disabled user groups with a highly user-centred design lifecycle. A new bi-level personalization approach was adopted which highlighted problems that had not been discussed in the literature (e.g. problems with synchronisation of media). This work has generated considerable interest from standards and industry groups (e.g. International Digital Publishing Forum, Health and Safety Executive) and has lead to research to develop an authoring tool to support accessible multimedia development.
Finding participants with particular characteristics (such as disability, age or particular experience) for usability evaluations can be difficult and can compromise the validity of the evaluations. Remote evaluations may provide a solution to this problem, but the relationship between face-to-face and remote evaluations is not well understood. Two studies were presented that provided the first detailed statistical and qualitative comparison of face-to-face and remote asynchronous evaluations. This paper was shortlisted for the "Best of CHI 06" award, meaning it was in the top 5% of papers accepted for the main conference in HCI, with an acceptance rate of 23%.
Usability has a specific, well-agreed definition, but varying lose definitions of accessibility exist. The relationship between the two concepts is widely discussed but not agreed. An innovative conceptual analysis of definitions of accessibility is undertaken, as well as possible relationships between accessibility and usability. Presents results of the first empirical investigation of the relationship between accessibility and usability, based on evaluation of two websites. Important findings on the lack of empirical validity of the widely used ratings of accessibility and usability problems are also introduced. Presented at CHI 07, the main conference in HCI, with an acceptance rate of 23%.
This study investigated psychophysical functions for perceived roughness for blind and sighted participants using the PHAMToM force feedback device. It has practical implications for the design of haptic interfaces and theoretical implications for roughness perception. It also has important methodological implications, showing that the pooled participant analysis used by previous researchers in analysing data from both physical and virtual roughness perception is incorrect and obscures important effects. Perception and Psychophysics is a highly cited journal (IF2003 1,856), chosen by a group of HCI experts as one of the 10 most influential journals in the field (Chen et al, BCS HCI 2005).
Since about 1970, rule-based graph transformation has been an active field of research with applications in many areas of computer science. This paper, for the first time, extends the mathematical theory of graph transformation to hierarchical graphs. In these graphs, hyperedges can again contain hierarchical graphs which allows an unlimited degree of nesting. The motivation is to structure large graphs in a comprehensible way and to reflect the hierarchical structure of systems in applications. The paper has been cited about 60 times (Google Scholar). Others have further extended our approach: see JCSS 68(3), 2003 and MSCS 15(4), 2005. This paper is a major revision and extension of a conference paper (not cited in the previous RAE). The journal paper gives full proofs for all results whereas the conference paper contains only proof sketches and some claims without proof. Moreover, the journal paper contains a new section with a case study which applies the paper's approach to the sorting of list graphs.
The double-pushout approach is the most mature approach to graph transformation. So far, however, almost all theoretical work has assumed that rules are matched by arbitrary, possibly noninjective graph morphisms - whereas implementations usually employ injective matching. This paper closes the gap between theory and practice by systematically developing the theory of graph transformation with injective matching. It proves that the injective approach is more powerful for both generating graph languages by restricted grammars and for computing graph functions by convergent transformation systems. The paper establishes all the classical commutativity, parallelism and concurrency results in this more expressive setting. It thus provides the theoretical foundation for existing and future implementations of graph transformation languages and systems. This paper is a major revision and extension of a workshop paper (not cited in the previous RAE). There are three new sections (in total 19 pages) and many new results.
An increasing number of languages for specification and programming by graph transformation are being designed, with applications in areas such as compiler construction or model-driven software development. This is the first paper to prove the completeness of a core programming language based on graph transformation. The language has a simple formal semantics and is minimal in that omitting any control construct leads to incompleteness. These results provide a theoretical foundation for the analysis of existing and the design of new graph-based languages. In particular, the core language is the basis of the programming language GP currently being implemented at York.
Knuth and Bendix showed in their seminal paper of 1970 that for terminating sets of term rewrite rules (directed equations), confluence (determinism) can be decided by the analysis of so-called critical pairs between rules. The present paper proves that for graph rewriting, the situation is inherently more difficult in that confluence is undecidable even for terminating systems. The paper then introduces critical pairs to graph rewriting and proves that these do provide a sufficient condition for confluence, albeit not a necessary one. These results are fundamental to the field of graph transformation and are of great practical relevance when it comes to checking that the input/output behaviour of computations is deterministic. This paper is a major revision and extension of a short book contribution, (not cited in the previous RAE). The extended paper proves the undecidability of confluence for graph rewriting whereas the short paper shows undecidability only for hypergraph rewriting. The undecidability proof is much simpler in that the number of rule schemata in the reduction of the Post Correspondence Problem decreased from 21 to 12. Moreover, the revised paper is rigorous with respect to the role of confluence modulo isomorphism, which was not worked out in the short paper.
Declarative languages are powerful, but their expressive power can be hard to characterise and tough to implement. The usual connection made between logic programming and classes of formal languages is based on sentential forms of computational trees. This paper instead gives a constructive proof that a restricted class of logic programs can be reduced to finite state machines. It also quantifies the conciseness gained over a more obvious logical encoding of regular languages, in which there is a doubly-exponential increase in the number of predicates needed. These results give both a definitive classification of expressive power and a route to new hybrid implementations.
This paper is the first to develop a formal model for the space of all possible uses of a purely functional data structure in the context of persistence and lazy evaluation. It shows how this model can be applied to automatic selection of data structures matching application characteristics such as the relative frequency of operations and single- or multi-threaded access. It gives results from tools based on the model, using program slicing and inductive classification methods to predict comparative performance of alternative implementations for a common data abstraction. The paper was selected for a special issue of JFP on algorithmic aspects of functional programming languages.
AFP is a biennial international Summer School: as leader of the Hat development team, I was invited to lecture on tracing and asked Koen Claessen (QuickCheck author) to join me; the other authors are Hat and QuickCheck collaborators. The chapter presents two innovative tool-kits for functional programmers. It demonstrates how the tools for testing and tracing can be combined effectively, not just in miniature exercises but in more demanding applications such as verifying congruence between interpreter and compiler for a small language. Associated materials were made available for downloading and the current Hat system has several hundred users world-wide.
This paper applies lazy functional programming to a demanding application: scientific visualisation. It gives new insights into the fine-grained pipelining possible in visualisation algorithms. It presents an unusually concise yet modular implementation of one family of such algorithms for surface extraction from 3D data. It demonstrates, using independently established datasets, that the lazy functional implementation is surprisingly competitive with the leading mature system programmed at a much lower level. The paper is a first-year output from a collaborative project funded under the EPSRC's programme for Computer Science Challenges in E-science. It was one of 63 from 228 submissions accepted for the top international conference in visualisation, with proceedings in a special issue of the IEEE journal.
Develops a new statistical Cartesian representation for directional data using azimuthal equidistant projection of surface normals. Leads to a novel linear model for 3D facial shape, that can be fitted to 2D brightness images to recover facial height. Overcomes several long-standing problems in facial shape-from-shading including concave/convex ambiguity and estimating facial albedo. Early version of paper accepted at ICCV 2005 (acceptance rate 20%). Work forms part of EPSRC MathFIT grant (Surface Reconstruction from Gauss Maps); final report rated Outstanding/Internationally leading.
Presents conceptually simple approach to problem of face shape recovery from one image: to learn the relationship between an image of a face and the corresponding 3D surface directly. Develops two frameworks for solving this problem using a novel form of statistical model which couples models of image brightness and 3D shape. Fitting the coupled models to images yields 3D shape in a way which avoids solving computationally expensive minimisation problems. This addresses the primary weakness of current state-of-the-art techniques. The resulting algorithms are computationally efficient and lead to accurate face shape recovery from real world images.
Interdisciplinary collaboration between psychology, computer vision and neuroimaging groups. Investigates viewpoint invariance of the neural representation of faces using Magnetoencephalography (MEG) scans. The phenomenon of adaptation was used to measure invariance to changes in viewpoint. Machine vision techniques were used to synthesise face image stimuli in varying poses. Acquiring such images in the real world, particularly for famous faces, is impractical. We show that the face-specific M170 response is viewpoint dependent, implying that the neural representation is also viewpoint dependent. First study to use advanced machine vision techniques to produce stimuli for the investigation of human visual processes. Journal impact factor: 6.187 (top 10% for neuroscience). Paper peer reviewed, accepted and appeared in advance access on 16/05/07 in final unpaginated form.
Develops statistical model for needle-maps using techniques from differential geometry and statistics of distributions on nonlinear manifolds. Demonstrates how irradiance constraints can be combined with the statistical model to robustly estimate face shape from single images. Robust statistics used to overcome classical problems in facial shape-from-shading of sensitivity to regions of low albedo and cast shadows. Shows how the technique can be used for illumination invariant face recognition given only a single training image. Previous state-of-the-art results used >7 images. Demonstrates links to spherical harmonic basis image representation. Early version of paper appeared in CVPR 2006 (acceptance rate 23%). Recent extension of work to gender recognition won Siemens Best Biometric Security Prize at BMVC 2007. Paper peer reviewed, accepted (27/06/07) and appeared in Springer IJCV online-first in final unpaginated form 9/08/07.
This journal paper is a revised and extended version of a paper presented at the GECCO 2005 international conference, which won a 2005 Human Competitive Awards ("Hummies") $1000 silver medal. The Hummies are the world leading award in Genetic Programming (GP). The paper describes the use of GP to evolve a general-purpose size-independent quantum algorithm to implement Shor's Quantum Fourier Transform, the basis of Shor's famous polynomial time factoring algorithm. This work demonstrates, for the first time, that automated computer-based techniques can be used to evolve significant quantum computing artefacts.
This journal paper is a revised and extended version of a paper presented at the ICARIS 2004 international conference. It lays out a multidisciplinary conceptual framework for a principled approach to the modelling, design and analysis of bio-inspired algorithms, providing for sophisticated biological models and well-founded analytical and computational principles, as opposed to ad hoc "reasoning by metaphor" in current use. The framework was developed as part of the EPSRC novel computation cluster "EIVIS" GR/S63823/01 (rated "outstanding"). The framework is applicable to bio-inspired computation in general; the paper describes applications to Artificial Immune Systems in particular. Various groups have already proposed to use this framework as a basis for their research in bio-inspired algorithm development.
This paper is published in two parts. (The second part is "II: Initial journeys and waypoints. IJPEDS 21(2):97-125 2006. DOI: 10.1080/17445760500355454".) It lays out the background, foundation, and initial proposals of UKCRC's Grand Challenge 7. The GC initiative provides a means for members of the UK Computing Science community to define long-term aims and opportunities for their discipline. The publication of this substantial statement of GC7 in an international journal has broadened appreciation of the UK's leading role in Computer Science, and has brought this particular challenge to the notice of a wider international audience. It has led directly to increased international collaboration in the area of Non-Classical Computing. (Stepney is the chair of Grand Challenge 7.)
This paper describes a numerical search technique used to discover highly entangled 4 and 5 qubit-states, of interest in the domain of quantum physics and quantum information theory. Publication of these computational results in an international physics journal has raised the profile of using numerical, computational techniques to discover interesting non-numerical physical results, where previously only analytical techniques had been used in this domain, and to lesser effect. It has helped these computational techniques cross boundaries between disciplines, aiding a multidisciplinary approach to quantum information theory.
We propose a framework for the development of Artificial Immune Systems (AIS). This paper was subsequently expanded into a book 'Artificial Immune Systems: A New Computational Intelligence Approach', which is widely used throughout the community as a major resource. We contextualise the AIS approach with other well known soft computing paradigms, such as neural networks and fuzzy logic, and propose mechanisms for the potential hybridisation of AIS with other such techniques. The impact of this work is the laying of foundational aspects of immune algorithms and representations within the framework.
This paper presents work that is a direct outcome of research funded by NCR plc. The paper details the development and prototyping of a real-time immune inspired system that is capable of predicting faults in automated teller machines (ATMs). The system is capable of adapting to new faults in ATMs. We have developed local adaptable error detection framework that is capable of learning new errors (on-line) both within an ATM and between a network of ATM's. Experimental evidence indicates that our approach is capable of identifying failure in an ATM up to 12 hours in advance. The work in this paper has led to 2 patent applications (reference Simon Forrest of NCR). This is the first major industrial application of AIS and will has a major impact on machine availability. Timmis was the lead researcher in the project.
This is an invited paper arising from a plenary lecture at the Workshop on Natural and Artificial Immune Systems, Italy, 2005. Here I set out a number of challenges to the AIS community that need to be addressed to make substantial progress. The impact of this paper is to bring to the fore requirements of AIS to: adopt a more formal approach to underpin the work with theory; to capture the complexity of the immune system more effectively with the use of richer biological metaphors through the use of principled modeling techniques and apply such solutions to demanding real-world problems.
This paper proposes, describes and analyses an immune inspired algorithm for a very challenging bioinformatics problem. We developed new mutation and aging operators which we found to greatly improve the performance of the algorithms, when considering the number of evaluations of the fitness function (a very important metric in this application, as the fitness value can take considerable time to compute). The impact of this work is the demonstration that immune-inspired systems can be as competitive, and in some cases outperform, some state of art on such a difficult problem.
Over the last 5 years I have been at the forefront of the international effort to turn the Java language and its environment into a viable technology for high integrity real-time systems. This paper represents my contribution. The work was developed during an EPSRC Grant (GR/M94113 - final grade: Tending to internationally leading). The work was used as the main input to a successful EU STREP project proposal (Top rated) called HIJA IST-511718, and is one of the main inputs into the current international attempts to define a standard for Safety Critical Java (Java Community Process: Experts Group for JSR 302).
Modern hard real-time systems (RTS) are underpinned by off-line schedulability analysis techniques. For fault-tolerance, run -time monitoring of resources is crucial to ensure the off-line guarantees are not undermined by the program's run-time behaviour. The Real-Time Specification for Java (RTSJ) is the first production-quality language to integrate this monitoring with its run-time scheduling. I have made significant contribution to its underlying theoretical model. This paper is the first to produce a formalism for analysing integrated approaches. The model is applied to the RTSJ's and a flaw is found. Achieved best paper at IEEE RTSS 2005 (the main RTS conference). The results are now being used to correct the RTSJ. Co-author is a research student of the author.
Presents a new performance indicator for analysing real-time garbage collection (GC) algorithms and uses this indicator to show the limitations of current GC approaches. A new algorithm is then developed whose motivations comes from the analysis of current GC algorithms. The approach is then integrated into modern scheduling theory using dual priority scheduling (which is novel for real-time GC algorithms) . The result both improves the current memory overheads of real-time garbage collectors and allows spare capacity at run-time to be used to ameliorate some of the inherent execution-time overheads. Both mathematical and experimental techniques are used to evaluate the performance of the collector. Chang is Research Student of the author.
Theoretical advances in real-time scheduling theory are held back by the lack of appropriate support in languages and run-time environments. York has pioneered the introduction of real-time programming language abstractions into the Ada 2005 standard. No other real-time programming language has such a comprehensive set of facilities. Rather than submit parts of the Ada language standard for review, this paper is submitted as evidence of the impact that York has had. The paper introduces the Ada mechanisms and shows how they can be used to program modern execution-time servers. These servers has previously been impossible to implement. The algorithms are evaluated in a simulated real-time environment.
Addresses the problem of graph representation and details a new approach for providing graph features from the eigenvalues and eigenvectors of the representation matrix. This is given a rigorous theoretical treatment using symmetric polynomials on real and complex algebras. Comprehensive experimental analysis is done on synthetic and real-world problems. The work forms part of an EPSRC project GR/M28613/01 rated internationally leading/outstanding and an earlier version of the work was awarded best paper at ACCV 2002. Method has been used in an EU INTAS project on protein structure matching with Moscow State University, BRIEM and UIIP Minsk, and University of Balearic Islands. Work proving influential in network analysis and architectural planning (Hanna).
This paper gives a rigorous mathematical treatment of the recurrent correlation associative memory (RCAM) model of Chiueh and Goodman. It shows how to optimise the performance of the memory under given noise conditions, how to compute the bit-error probability after an iteration of the memory and gives a predictive model of the recall error rate of the memory. This is an important advance in the understanding of such memories and enables the design of better RCAM models. Work influences papers of Du et al and Pavloski et al in TNN. An abstract describing a preliminary stage of this work appeared in ICPR 2000 but was not used in the previous RAE. The archival journal version appearing in TNN 2003 describes a significantly improved analysis of the RCAM and additionally gives a) an in-depth literature review, b) a detailed and rigorous theoretical analysis of the error probability using a detailed pattern space model, c) an analysis of the storage capacity of the RCAM, d) a full experimental evaluation of the method including a detailed sensitivity analysis and an in-depth comparative study.
This paper uses a probabilistic tuning function and a mixture model of von Mises distribution to describe the output of a Gabor filter bank on the image. This allows the description of orientation structure in a principled and analytic way, giving a probability density function of the local orientation. This is determined using parameter estimation procedure based on the EM algorithm. This is a notable contribution to the analysis of Gabor filter banks and is also of interest to the neuroscience community who study populations of orientation-tuned neurons. The first author is an RS supervised by Wilson.
One of the first papers to use embedding on spectral features of graphs. Novel graph features are proposed based on spectral clusters. The effectiveness of these features is gauged by embedding them using techniques such as ICA, PCA and MDS. The result is a powerful and efficient new way of representing the structure of graphs. The work forms part of an EPSRC project GR/N33348/01 which was rated internationally leading/outstanding. This work has lead to a resurgence in spectral methods for graphs and has influenced work in the University of Toronto and Australian National University.
Access to to resources and data in open distributed systems is difficult to control. The conventional access control list is highly centralised and thus does not scale well. Although 'capabilities' have been shown to be a solution to this distribution problem, they cannot be uniformly applied to tuple-space systems. This work generalises capabilities to apply to types rather than just objects, enabling access and visibility control to be incorporated into open distributed systems. The ways in which multi-capabilities can be combined are treated formally and an implementation of the concepts in a tuple-space coordination system, and analyses its performance.The results show how users of such systems can achieve private communications, and a finer degree of resource management than was previously possible.
Open distributed coordination architectures must be scalable. This paper analyses and discusses the implications of this necessity in the context of tuple-space systems, pointing out the opportunities offered by such systems as well as the difficulties. The analysis follows a framework previously defined by Cardelli, and structures the arguments in terms of the four properties of a system of which an agent can be aware. This work has developed into several avenues of research including those detailed in the other submissions.
This paper introduces a novel approach to the problem of incorporating time into the atemporal tuple-space model of distributed systems. Previous approaches have often taken the route of adding timeouts to the access operations, but these are argued to be inherently flawed. The new approach uses the idea of 'fading' from work on Swarm Intelligence to supply a variety of local time without encountering the difficulties identified for ad hoc timeouts. Applications include (non-conservative) garbage collection and adaptive tuple retrieval.
Distributed tuple-space systems rely on matching of types to retrieve data, and all existing systems use a single language to achieve this. However, open systems must support all languages and thus types and their representations cannot be language specific. This paper addresses this problem by using type isomorphisms automatically generated from a neutral type specification language. The results of an implementaton are used to demonstrate the feasibility and usefulness of the technique.
This is the first formal semantics for the Handel-C language for programming FPGAs: it gives a precise characterisation of prioritised choice, the construct responsible for most of the semantic complexity of the language. The semantics is the first unifying theory (in the sense of Hoare & He) of synchronous hardware, state-based programming, and message-based paradigms). This was an invited paper in a special journal issue on formal methods for industrial critical systems. The work has led to a doctoral studentship, project proposals to EPSRC and Science Foundation Ireland, and collaboration with Celoxica.
This paper combines in Unifying Theories of Programming for the first time four different paradigms of programming: imperative, concurrent, message passing, and object orientation. It's a tricky business getting these four aspects to compose, and this paper manages to achieve it using the UTP approach. In passing, it solves some intesting problems, such as the meaning of method calls in pre and postconditions (even in negative positions), and the role of visibility constraints in specifications. The latter are treated in a novel way as code, and so need not be strictly enforced abstractly; this approach leads to more flexible and natural specifications. The paper was an invited submission to a special journal issue on combining state and event-based paradigms.
This paper introduces a mathematical formalism to reason precisely on how to schedule and analyse systems with a guaranteed number of deadline misses using the notion of weakly-hard constraints. Mathematical proofs of systems specified with those constraints prove that the schedulability of systems can be improved by using such methods. This work shows that provable bounds on the number and distribution of deadline misses can be provided.This work has been taken up by and extended by other authors into on-line scheduling approaches and different process models, communication systems, and scheduling of control systems. (Llamosi was Bernat Ph.D. supervisor)
This paper proposes a set of morphological operators used for 3-D shape interpolation from sparse cross-sections. Two mathematical morphology operators that combine selective dilations and erosions are used to morph one cross-section into another, resulting in a smooth series of sections through a volume. The proposed methodology was applied to artificial data as well as to volumetric medical images providing comparisons with ground-truth and other approaches. The results of this research have influenced the work of research groups in biomedical sciences from U. Laval (Canada) and Georgia Tech (USA).
This paper describes for the first time a complete analysis of radar shape from shading that rigourously considers each stage of processing from reflectance estimation to surface integration. 3-D terrain height information is derived using the radar luminance function, the radar signal statistics as well as uncertainties in the estimation of topographic features. Each processing stage of the system is independently analysed, and the results assessed numerically as well as through comparative studies. The EPSRC research project that funded this work "Terrain Analysis using Radar Imagery" has been rated internationally leading/outstanding. This paper was principal precursor to Hancock's EPSRC MathFIT follow on grant `Surface Reconstruction from Gauss Maps'. A description of a preliminary version of the algorithm appeared in CVPR 2000 as an oral presentation but was not used in the previous RAE. The PAMI 2003 paper extends the CVPR paper from surface normals to terrain height reconstruction, providing a) an in-depth analysis of the problem, b) detailing a novel surface integration method c) providing extensive experimental results on real world images.
This paper introduces a new approach for 3-D watermarking of graphical models in the spatial domain. The originality of the approach consists in developing a new method for applying controlled perturbations onto meshes representing graphical objects. A rigorous study of the effect of perturbations on meshes is provided in the paper. The paper is significant in the watermarking field because it provides for the first time a thorough analysis of 3D watermarking methods using local perturbations by considering the local geometry. The significance of the results is emphasised in papers published by groups from U. Firenze, U. Thessaloniki, U. Aachen, U. Magdeburg, etc.
This paper introduces a new nonparametric classification method using the quantum mechanics principles. The originality of the approach consists in deriving a new kernel scale estimator to be used with the Schrodinger equation as a clustering measure. The proposed nonparametric clustering methodology is rigorously described in the paper starting with the estimation of the kernel scale until the separation of the clusters. The significance of the paper is twofold: firstly, a new kernel scale estimator is provided and secondly, quantum clustering is employed for blind segmentation of terrain using the topography information. N. Nassios was a PhD student.
This paper provides the first experimental demonstration of quantum telecloning - a communication protocol for quantum systems that combines teleportation (disembodied transport) with cloning (copying). Quantum telecloning allows an eavesdropper to tap a quantum communication channel in a guaranteed anonymous fashion, hence potentially weakening the security of commercially available quantum cryptographic systems. The experiment reported here telecloned laser light (coherent states) with a fidelity which guarantees that the clones were distributed via a quantum communication channel. The submitter devised the protocol, was heavily involved in the experimental design and wrote large portions of the manuscript. The work has received favourable responses both in the scientific community (Nature's Research Highlights, 23 Feb 2006; New Scientist, 21 Feb) and in the popular press (The Scotsman, 17 Feb; The Advertiser, 18 Feb).
Continuous variables allow for the effective implementation of many quantum communication protocols, including teleportation, dense coding, cryptography, error correction, and more. However, it was unclear to what extent they could be used to also perform computation. This paper proves that the simplest sets of operations which can achieve so many communication protocols are actually insufficient for full computation with continuous quantum variables. This led to a renewed (and ongoing) effort to find efficient, yet near noiseless, implementations of the required extended operations. This paper was included in the March 2002 issue of the Virtual Journal of Quantum Information.
Telecloning naively combines the quantum teleportation and quantum cloning protocols. It allows multiple (approximate) copies of a quantum state to be distributed remotely. Remarkably, in this paper we prove that telecloning itself forms a new quantum information processing primitive which may be performed in one step with fewer quantum resources (less entanglement) than any combination of cloning and teleportation. This theoretical analysis inspired the first experimental demonstration of telecloning by the author and collaborators at the University of Tokyo [Phys Rev Lett 96, 060504 (2006)]. This paper was included in the January 2002 issue of the Virtual Journal of Quantum Information. [The manuscript appeared on the LANL arXiv on 13 December 2000 and was submitted to Physical Review Letters the following day. After review, a revised manuscript was submitted on 22 August 2001 and was published on 26 November 2001.]
The no-cloning theorem of quantum mechanics forbids the exact cloning of an arbitrary quantum state. However, inexact cloning is possible in theory. In this paper we show theoretically that the quantum states naturally generated by lasers (coherent states) may be optimally cloned by linear optics (a series of beam splitters) and optical amplification. This work shows how the quantum limit to multiplexing laser-encoded information may be achieved. This paper has spurred a large amount of work on cloning coherent states, attaining 57 citations already. Indeed, our scheme has been implemented experimentally in Germany [Phys. Rev. Lett. 94, 240503 (2005)] by moving the optical amplification off-line.
This paper derives response time analysis that can accommodate fault-tolerant structures for real-time systems scheduled under the most common policy of fixed priority dispatching. The analysis extends work first presented at the international conference ECRTS01. This analysis is the first that allows the per-task fault recovery code to be scheduling at different priorities to that of the normal code. The paper also derives a feasible and optimal priority assignment algorithm for this recovery code. Optimal is the sense of maximising fault resilience. Lima was a PhD student of Burns.
Challenges the existing role of model checking for real-time systems. Rather than attempt to check all temporal properties (which has proved impossible for all but the smallest system) scheduling analysis is retained as the means of ensuring an implementation will meet its deadlines. The validity of the deadlines themselves is model checked using a Timed Automata model that distinctly only allows progress when deadlines pull forward execution or delays are specified. An outcome of an EPSRC project:Ravenspark (Rated Alpha-4). Application of this work has been taken up by Praxis within its SPARK technology (Rod Chapman is the contact).
A large volume of research material for soft (i.e. not hard) real-time systems uses the notion of utility (or value) to determine which tasks should meet their deadlines during system overload or when QoS concerns would indicate that online decisions need to favour particular tasks. This research is however significantly undermined by the lack of clear semantics for utility. This journal paper is the first to develop a measurement-theoretic model for utility and characterises the various notions and uses of utility. An outcome of a EPSRC project: Vastu (Rated Alpha-4). Prasad was RS on project.
This paper provides the first formulation of scheduling analysis to allow event-triggered approaches to computation and communication to provably protect themselves against a babbling node that would otherwise undermining the temporal behaviour of the system. A bus-guardian and associated scheduling approach is developed for a CAN-like protocol. This paper, together with others from York and elsewhere, convincingly argues for the use of the more flexible and resource efficient event-triggered approach over the more conservative time-triggered approach, even for safety-critical systems. Broster was a PhD student of Burns.
This paper uses Markov models to define measures of usability with push button devices and hence to suggest modifications to devices that would improve usability in the dimensions measured. Unlike previous approaches to usability measures, these measures are statistical and allow for erroneous rather than optimal or deterministic behaviour. Additionally, the approach is founded on well established mathematics and the underlying models are finite-state machines. These features mean that the measures are recognised (for example, in the works of Paterno et al, Kajimata et al, and Massink et al.) as a stochastic modelling approach complementary to formal methods analyses.
This paper describes a user interface for authoring articles for the substantial Mizar library of formal mathematics. Additionally, a search tool is integrated into the authoring process and uses latent semantic indexing to provide search results that are semantically closer to the query than syntactic or logical searches can provide. This user-centred approach to interface development for mathematical knowledge management has not been previously considered. Though relatively recent, the work has been informally received at MKM conferences as an unusual yet promising approach to formal mathematics and the representation of mathematical knowledge
This paper uses grounded theory to examine how children engage and are immersed in an interactive museum exhibit situated at the Science Museum in London. Whilst museums are keen to provide positive learning experiences to children, evaluation of exhibits is difficult. Our work provided valuable insight into the impact of the particular exhibit and opened up the possibility of evaluating engaging user experiences for the HCI community, in particular, the use of grounded theory to provide a rigorous understanding of the actual experiences of children.
This paper uses user-centred methods to develop and evaluate a digital presentation of a mathematics course. This was the first fully user-centred approach in the area of mathematical knowledge management (MKM) and its importance was recognised as the authors became lead investigators on a usability package in the EU funded MKM network (IST-2001-37075). The representation and content used was also integrated into the European funded LeActiveMath project (IST-2002-2.3.1.1.2) for producing and delivering mathematics courses interactively.
Woodcock et al's Angel tactic language uses angelic nondeterminism to search for proofs in mechanical theorem proving attempts, and it has been implemented by researchers at Oxford, Queensland, Recife, and Turku. This paper makes significant semantic extensions to Angel to search for program refinements whilst accumulating verification conditions. This tames the refinement calculus by allowing strategies to be recorded precisely and used as single transformation rules. The result is a unique refinement tactic language that has a denotational semantics, a proof theory, and a refinement theory of its own, allowing tactics to be verified and developed just like any other program.
Although the pi-calculus is hugely successful as a theoretical arena in which to study the computational phenomenon of mobility, the role of mobile processes and channels in program development is less well-studied. Where do they come from? Is it possible to introduce mobile processes to implement specifications with no mobility? These questions --and others-- are answered by a theory of refinement for mobile processes based on a denotational semantics. This paper sets out for the first time the theoretical basis and development technique for mobility, illustrating it with the practical programming language occam-pi, which blends occam and the pi-calculus. The Mathematics of Program Construction Conference is the leading conference for the presentation of such results. The work was the basis for a research contract and studentship funded by QinetiQ.