UNderstanding COmplex system eVolution through structurEd behaviouRs (UNCOVER)

The project aims to develop theories and implement prototype software tools for the formal verification, synthesis and analysis of *complex evolving systems*. Such systems may involve hardware, software and human organizations; though very common in practice, as yet such systems lack robust scientific and engineering support. The project will do this by developing a rigorous methodology supported by a toolkit based on structured behavioural representations (structured occurrence nets). The effective use of such representations greatly reduces the cognitive complexity of, and the storage and computational resources involved in the modelling and manipulation, of large systems. Moreover, it offers a solution to the difficult problem of representing and analyzing the behaviour of systems that are evolving, e.g. through being subject to modification (by other systems). The power and generality of the new formalism of structured occurrence nets, and the potential of our planned toolkit, will be demonstrated using three case studies: (i) the verification of asynchronous VLSI circuits, (ii) on-line deadlock detection in networks-on-a-chip, and (iii) in partnership with a leading commercial developer of such systems, a major crime investigation support system.

The prime beneficiaries of UNCOVER are aligned with the planned case studies. One large group of beneficiaries, related directly to our Task-III-C case study, are organisations and companies who make use of investigation support software. For example the various police authorities, trading standards organisations, and a number of other government organisations, use such software in support of criminal investigations and any subsequent judicial proceedings. In addition large commercial organisations use it in support of internal investigations into suspected frauds, etc. Many of these are long-standing clients of our industrial partner CLU, a market leader among developers of investigation support systems, so will be well-positioned to benefit directly from our planned work on improved infrastructural facilities for failure analyses, work that should enable CLUE's future software to deal with larger and more complicated sets of investigation data and evidence, arising from more complex evolving crime situations, than is currently practical. More generally, our Centre for Computer Security and Cybercrime, with its close links to the National Fraud Forum and its constituent regional bodies, will provide a unique and very effective communication channel to a large number of public and private sector organisations who have a direct interest in improved tools and techniques for investigating cries, in particular cybercrimes.

More generally, this aspect of our proposed research and its outcomes should also influence social networking providers, medical professionals and trusts, large financial institutions, and other end users maintaining large records of dynamically changing data, and who currently typically have to use general purpose relational database systems, incorporating ad hoc sets of relations expressing any known causalities, for their records. They will be able to use instead the theoretically well-grounded techniques developed by our project for representing causality in complex evolving situations, and so gain increased understanding of, and enhance their ability to analyse and exploit, the content of their databases.

Another group of direct beneficiaries, from our planned work on two further case studies - Task III-A (Static Analysis) and Task III-B (Online Deadlock Detection) - are the designers, implementers and users of computer-aided tools for asynchronous systems with stringent power constraints. Particularly notable among the set of industrial developers and users of such electronic design automation systems with whom we have long-standing close links are Intel and Phillips. Their continuing close interest in system modelling and verification, both prior to and following initial deployment, is such that they should be well-placed to take up and exploit the results of these two case studies, and the research that they demonstrate, very directly.

Through this second group of beneficiaries the proposed research on system validation and its outcomes will also influence, through its potential impact on the tools available to them, large industrial enterprises, manufacturers and users of networked technologies, and designers and users of complex embedded systems. In all these cases, the impact on short and long term beneficiaries will be through novel means of understanding the dynamic behaviours of systems in their specific domain, as well as through providing robust support for their design, implementation and system maintenance activities.