Welcome to the Research Project Website for the UNCOVER project.
UNCOVER was a project run by Newcastle University's School of Computing Science and funded by the EPSRC. It involved researchers from the School of Computing Science and the School of Electrical and Electronic Engineering.
The project aimed to develop theories and implement prototype software tools for formal verification, synthesis and analysis of complex evolving systems. Typical examples are a large hardware system which suffers component break-downs, reconfigurations and replacements, a large distributed system whose software is continually updated (or patched), a multi-organisational computer system whose human operators undergo regular re-training, or a typical large bureaucracy. The importance of structure in helping designers to cope with design complexity is well-accepted, especially in the software engineering and VLSI design domains. The effective use of such structuring notations greatly reduces the cognitive complexity of designs, and the resources, both storage and computational, involved in their representation and manipulation. The UNCOVER project, which was centred on the use of a new formalism, structured occurrence nets (SONs), aimed to bring similar benefits to the problems of representing and exploiting representations of system behaviour (as opposed to design).
Key finding and achievements of the project:
The SONcraft tool that was developed in UNCOVER is a very general purpose one, potentially applicable in a variety of domains. The initial motivation behind its development was the problem of analyzing the causes of failures in complex computing systems, but in fact the application domain that was concentrated on was crime investigation, and the project has had numerous very useful interactions with a number of police and other investigative agencies, and tool suppliers to these agencies. One likely future development is the incorporation by the Clue Computing Co. of SONcraft-like facilities into their CLUE investigation support system. Another example of potential non-academic impact of work carried out within UNCOVER concerns the XMAS modelling language. It has been proposed by Intel for designing communication fabrics of complex many-core systems on chip. The developed tools have been made available to the systems design community, and we expect that some practical take up will be in private and public sectors, including organisations developing networks on chip. In addition, throughout the project, the UNCOVER team investigated the interplay between different concurrency models. It was discovered that Conditional Partial Order Graphs (CPOGs) have a succinct and elegant algebraic characterisation, which led to the work on new domain-specific languages for the compositional design of asynchronous circuits and processor instruction sets. Furthermore, it was demonstrated that CPOGs have advantages over other concurrency models in terms of compactness and ease of comprehension by designers. Further research and development work on this topic is being pursued in collaboration with Dialog Semiconductor.