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.

Publications

10 25 50
publication icon
Mokhov A (2014) Algebra of Parameterised Graphs in ACM Transactions on Embedded Computing Systems

publication icon
Jezequel L (2015) Factored Planning From Automata to Petri Nets in ACM Transactions on Embedded Computing Systems

publication icon
Germanos V (2015) Diagnosability under Weak Fairness in ACM Transactions on Embedded Computing Systems

publication icon
Janicki R (2015) Step traces in Acta Informatica

publication icon
Ponce de León H (2018) Compact and efficiently verifiable models for concurrent systems in Formal Methods in System Design

publication icon
Janicki R (2015) Characterising Concurrent Histories in Fundamenta Informaticae

publication icon
Fernandes J (2015) Persistent and Nonviolent Steps and the Design of GALS Systems in Fundamenta Informaticae

publication icon
Burns F (2017) A Structured Visual Approach to GALS Modeling and Verification of Communication Circuits in IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems

publication icon
Karkar A (2018) Network-on-Chip Multicast Architectures Using Hybrid Wire and Surface-Wave Interconnects in IEEE Transactions on Emerging Topics in Computing

publication icon
Mokhov A (2015) Algebra of switching networks in IET Computers & Digital Techniques

publication icon
Mikulski L (2014) Folded Hasse diagrams of combined traces in Information Processing Letters

publication icon
Koutny M (2017) An extension of the taxonomy of persistent and nonviolent steps in Information Sciences

publication icon
Janicki, R. (2013) Causal Structures for General Concurrent Behaviours} in International Workshop on Concurrency, Specification and Programming

publication icon
Janicki R (2019) Classifying invariant structures of step traces in Journal of Computer and System Sciences

publication icon
Khomenko V (2013) A Polynomial Translation of pi-calculus FCPs to Safe Petri Nets in Logical Methods in Computer Science

publication icon
Shafik R (2020) Harmonizing energy-autonomous computing and intelligence: an editorial introduction. in Philosophical transactions. Series A, Mathematical, physical, and engineering sciences

publication icon
Khomenko V (2013) Direct Construction of Complete Merged Processes in The Computer Journal

publication icon
Bonet B (2014) Recent advances in unfolding technique in Theoretical Computer Science

publication icon
Kleijn J (2017) Applying regions in Theoretical Computer Science

publication icon
Rafiev A (2013) ArchOn

publication icon
Bowen Li (2015) Unfolding CSPT-nets

publication icon
Mokhov A (2017) Process Windows

 
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