UNCOVER

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:

  • We extended the fundamental model of structured occurrence nets (SONs) with new features related to alternate behaviours and timing information. We implemented all basic functionalities in the SONCraft toolset integrated into the Workcraft environment, and made it available for public use. SONCraft provides, in particular, a user-friendly graphical interface that facilitates model entry, supports interactive visual simulation, and allows the use of a set of analytical tools for the reachability analysis.
  • We have obtained a full characterisation of causality structures which underpin execution histories represented by SONs. They are built from strong causality, weak causality and mutex relationships which are linked by a set of intricate axioms. We also provided a language theoretic counterpart of these structures in the form of step traces corresponding to sets of step sequences generated by SONs.
  • xMAS models are a new communication paradigm which can be used to model circuits and networks for the purpose of synthesis, testing and verification. Previous attempts at synthesis and verification of xMAS models have been proposed for synchronous implementations only. Novel GALS synthesis and verification environment, theory, algorithms and tools, have been developed for xMAS, which are based on the structured occurrence nets. The tools have been integrated into the Workcraft environment and made available for public use.
  • Conditional Partial Order Graphs (CPOGs) can be used for compact representation of behaviour of concurrent systems as an alternative to event structures and Petri Net unfoldings. An algebraic characterisation of CPOGs has been developed.
  • New algorithms for direct construction of merged processes and contextual merged processes been developed and implemented, paving a way for their introduction in SONCraft.
  • A polynomial translation of pi-calculus finite control processes to safe low-level Petri net has been developed and implemented, and methods for using Petri nets to verify opacity, security, and other behavioural properties in distributed cloud systems have been proposed.
  • The applicability of verification techniques based on Petri net unfoldings has been advanced by strengthening several results in the core of the theory of Petri net unfoldings, and thus making them available for the introduction in structured occurrence nets; in particular, a new notion of diagnosability under the weak fairness assumption has been proposed.
  • We developed new relationships between Petri nets on which SONs are based and different kinds of temporal logics, and invented novel ways of dealing with the persistence and nonviolence in the behaviours of Petri nets. We also developed algorithms for the synthesis of nets with localities from their behavioural specifications given in terms of finite step transition systems.

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.