UNderstanding COmplex system eVolution through structurEd behaviouRs (UNCOVER)
Lead Research Organisation:
Newcastle University
Department Name: Computing Sciences
Abstract
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.
Planned Impact
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.
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.
Publications
Khomenko V
(2017)
Formal Design and Verification of an Asynchronous SRAM Controller
Tarawneh G
(2017)
Xprova: Formal Verification Tool with Built-in Metastability Modeling
Karkar A
(2018)
Network-on-Chip Multicast Architectures Using Hybrid Wire and Surface-Wave Interconnects
in IEEE Transactions on Emerging Topics in Computing
Ponce de León H
(2018)
Compact and efficiently verifiable models for concurrent systems
in Formal Methods in System Design
Beaumont Jonathan Richard
(2018)
Compositional circuit design with asynchronous concepts
Ikenmeyer C
(2018)
On the complexity of hazard-free circuits
Janicki R
(2019)
Classifying invariant structures of step traces
in Journal of Computer and System Sciences
Description | We developed the notion of structured causality supported by an interactive tool in order to model and reason formally about complex evolving systems using structured occurrence nets. A structured occurrence net is a collection of occurrence nets - finite directed acyclic graphs with nodes representing states or events and directed arcs representing causal links that collectively represent a single execution or 'run' of a system - related (i.e. structured) through communication and abstraction relations. An occurrence net represents system execution from an initial state that provides the context in which an event can occur, which causes a transition to one or more other states that lead to the occurrence of further events, and so on until a final system state is reached. A structured occurrence net represents an execution of a system of systems, and in fact of a system viewed at different levels of abstraction. The latter enables the cognitive complexity of a complex evolving system model to be reduced significantly, and the graphical representation of a structured occurrence net facilitates model visualisation. The evolution of a complex evolving system is represented by relating different occurrence nets representing different versions of the system to an occurrence net at a higher level of abstraction that creates the different versions. The use of causality as the fundamental relationship between states and events enables the modelling and analysis of causes and their effects, as well as of hypothesized causes and predicted effects. This is useful for analysing system failures and for modelling provenance. However, the applicability of structured occurrence nets is very much wider, because causality is the basis of Science, Engineering, and Rational Investigation domains in general. |
Exploitation Route | By applying structured occurrence nets to different application areas. |
Sectors | Aerospace Defence and Marine Communities and Social Services/Policy Digital/Communication/Information Technologies (including Software) Electronics Manufacturing including Industrial Biotechology Security and Diplomacy Transport |
Description | XMAS modelling language 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 takeup will be in private and public sectors, including organisations developing networks on chip. 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. |
First Year Of Impact | 2016 |
Sector | Electronics |
Impact Types | Economic |