Summary of the impact

Newcastle University's fundamental research into the theory of concurrency and the automated construction and analysis of asynchronous systems has resulted in novel technologies that have been adopted and applied worldwide by industry. This case study describes impact over the last five years on the industrial development of asynchronous microprocessor chips, in particular, deployed by Intel for handling financial transactions on NYSE and NASDAQ (with combined daily volume of trade exceeding £80 billion), and the improvements in business process analysis through the world-leading open-source ProM tools (downloaded over 65,000 times since 2008, and used by a number of major organisations, e.g. ING Bank and Deloitte).

Underpinning research

Automated construction (synthesis) is an engineering approach which aims to build models of systems from full or partial specifications of the systems' required dynamic behaviours. In particular, it supports a correct-by-design way of developing new asynchronous hardware and software systems, and is the only viable alternative to the very costly task of ensuring the correctness of such systems through an exhaustive exploration of their possible behaviours. Synthesis can also be used to elicit intrinsic patterns of behaviour from actual records of the operation of highly complex systems — e.g. large business organisations — in order to understand and improve the interactions within such systems. The research described here has, in a fundamental way, advanced the synthesis and formal analysis of complex asynchronous systems. Its main findings resulted from the long-standing investigations conducted at Newcastle University within two interrelated strands of research:

(i) the design of asynchronous (self-timed) VLSI circuits, led by Alexandre Yakovlev (Lecturer/Reader/Professor of Computer Systems Design: 1991 - present), and

(ii) the theory of concurrency, led by Maciej Koutny (Lecturer/Reader/Professor of Computing Science: 1994 - present).

This research was carried out jointly with Victor Khomenko (Demonstrator/Lecturer/EPSRC External research fellow/Lecturer/Senior Lecturer: 2003 - present) and Marta Pietkiewicz-Koutny (Research associate/Lecturer: 2000 - present).

The main outputs of the research have been theories, algorithms and tools for synthesis and analysis of asynchronous systems. Research on asynchronous system synthesis and analysis was initiated at Newcastle University in the 1990s by Alexandre Yakovlev who developed the first formal model of the concurrent behaviour of asynchronous VLSI circuits, based on Petri nets extended with annotations representing the switching behaviour of the circuits being modelled. The resulting Signal Transition Graphs (STGs) model [P1, P2] has become a standard notation for designing controllers and interfaces in multi-synchronous systems on chip. After adopting an analytical approach based on partial order concurrency semantics, investigated by Maciej Koutny since the 1980s, Petri nets together with the associated algorithms and tools moved to the centre of the new asynchronous system design flow, and now play a role similar to that of finite state machines in the well-established synchronous system design.

There are two main components to Newcastle's foundational research results which underpin the impact described in this case study: (i) the development of STGs together with efficient formal analytical techniques [P4,P5], and (ii) the development of techniques and tools for the synthesis of asynchronous systems [P2, P3, P6]. The formal analytical techniques are based on the finite complete prefixes of net unfoldings which are acyclic Petri nets representing the entire state spaces of the original STGs in a way which alleviates the state space explosion problem. By being based on the partial order representation of concurrent behaviour, net unfoldings represent in a direct way the inherent causal relationships in the operations of STGs and can therefore support, in particular, efficient model checking of behavioural properties such as deadlocks, and succinct visualisation of signal encoding conflicts which are needed for any practical circuit design flow. The techniques and tools for the synthesis of asynchronous systems are based on the theory of regions of transition systems. A transition system provides behavioural specification of the concurrent system (e.g. STG or Petri net) to be constructed, and its regions are used to build the components such as local states and connections between local states and actions. The resulting model exhibits the required behaviour, if such a realisation is at all possible, and the method provides vital feedback if the required behaviour is inconsistent or impossible to realise. In 2002 the Newcastle University team, together with collaborators from EU and USA (working for Cadence and Intel), produced the software tool Petrify which among other functions can synthesise STGs from transition systems, and is capable of building Petri net models from large sets of event logs. Petrify was selected as a finalist of the prestigious EU DESCARTES prize in 2002.

References to the research

Key Research Grants

The reported research was primarily supported by EPSRC:

[GR/L93775] £162,000, 1/05/1997-31/10/2001, Asynchronous communication mechanisms for real-time systems (COMFORT), PI: A. Yakovlev. Final assessment: research quality — internationally leading, overall — outstanding.

[GR/M99293/01] £55,793, 1/1/2000-31/12/2002, A system for parallel model checking, PI: M.Koutny. Final assessment: research quality — internationally leading, overall — outstanding.

[GR/M94366/01] £173,057, 1/3/2000-28/2/2003, Model visualisation for asynchronous circuit design (MOVIE), PI: A. Yakovlev. Final assessment: research quality — tending to internationally leading, overall — tending to outstanding.

[GR/R16754] £325,000, 1/07/2001-31/09/2004, Behavioural synthesis of systems with heterogeneous timing (BESST), PI: A. Yakovlev. Final assessment: research quality — internationally leading, overall — outstanding.

[GR/S12036] £244,563, 1/01/2003-31/12/2005, Synthesis and testing of low-latency asynchronous circuits (STELLA), PI: A. Yakovlev. Final assessment: research quality — internationally leading, overall — tending to outstanding.

[EP/C53400X/1] £264,357, 1/9/2005-31/8/2010 (RAE and EPSRC Fellowship), Design and verification of asynchronous circuits (DAVAC), PI: V.Khomenko.

Details of the impact

The research described in Section 2 produced novel tools and technologies that have been adopted by academia and industry. We present the impact in the two distinct areas: industrial asynchronous circuit design; and business process mining.

The research has enabled automated construction of asynchronous circuits
Gartner Analysts reported that for the years 2010-2012 the total annual worldwide semiconductor revenue was on average $300 billion. Intel Corporation had 16% of this market and was the world leading manufacturer of processor chips for high-performance computers ("no.1 semiconductor vendor for the 21st year in a row"). One of the fastest growing areas of semiconductor manufacturing is concerned with asynchronous circuits, which are faster and have lower power consumption than the existing synchronous ones; e.g., as stated by Fulcrum Microsystem (acquired by Intel in 2011): "Fulcrum Microsystems' [asynchronous] switch silicon, already recognized for high performance and low latency, complements Intel's leading processors and Ethernet controllers, and will deliver our customers new levels of performance and energy efficiency while improving their economics of cloud service delivery." [E9].

The results of research described in this case study have been used as the basis for Intel Corporation's Computer Aided Design (CAD) tools for asynchronous circuits. In his letter [E2], Intel's Chief Scientist for Technology Development identified the longstanding problem of high levels of complexity that the inherent concurrency of asynchronous circuits pose to industrial designers, and stated that "The predominant means of analysing this concurrency is Petri Nets and the work by Alex Yakovlev and his colleagues have pioneered the application of Petri Nets to asynchronous circuits" [E2]. Specifically STGs, Petrify and related Petri net theories have provided:

(i) the basis of understanding and modelling performance analysis as well as optimisation of asynchronous circuits, and

(ii) the formal basis of the slack matching optimisation algorithm (patented by Fulcrum Microsystems [E1]) which is a key technology for asynchronous circuits design.

In combination, together, (i) and (ii) have allowed Intel to produce higher performance asynchronous circuits ("Slack matching is one of the core technologies within the asynchronous CAD flow that my Intel division is using and this process is a pillar to us achieving higher performance than the synchronous alternatives in our past two products" [E2]). The impact is already evident in the wide deployment of the new circuits in the financial services industry; in particular, most transactions on the NYSE and NASDAQ (combined daily volume of trade exceeding £80 billion) now rely on Intel's switch silicon — a design facilitated by the use of new CAD tools that depend on the research described in this case study [E2].

The research described in Section 2 is now an embedded element of teaching practice in asynchronous design, demonstrating that this vital area of professional training has been informed and stimulated by research at Newcastle University. Around the world, most of the top engineering courses use Petrify and STGs in courses on asynchronous circuit design (e.g. Columbia University, Technical University of Vienna, and IIT Delhi). As Intel's Chief Scientist for Technology Development [E2] testifies: "The tool Petrify and STGs have become a fantastic means of teaching and explaining asynchronous design concepts".

Improved business process analysis by practitioners & large organisations
Process mining is a fast-growing area of business process analysis which allows practitioners to discover, monitor, and improve business processes by extracting knowledge from event logs. Research on asynchronous system synthesis and analysis at Newcastle has provided tools and methods that can significantly enhance the effectiveness of the analysis of complex business processes that involve parallelism. The resulting process mining technologies allow the beneficiaries to improve their system models, leading to the improved performance of the organisations themselves. This is especially important for complex organisations with several parallel business processes.

The Process Mining Group (http://www.processmining.org/) incorporated Petrify into ProM [E3], a generic world-leading open-source framework and toolset for supporting process mining through a two-step construction process. The second step, the discovery of control flow processes based on example event logs, is implemented using the Petrify tool [E3, E4, E5].

ProM tools have been downloaded over 65,000 times since 2008 and have been used to analyse event logs of over 100 organisations [E3, E6] including: ING Bank, DSM, Deloitte, Philips Healthcare, Ricoh, Thales and Winkwaves. The analysis of event logs using ProM has been carried out for a variety of purposes and benefits, e.g.:

- In the Dutch AMC hospital it was used for analysis of billing information of about 627 gynaecological oncology patients resulting in understandable models for large groups of patients (2008 [E7]), allowing streamlining processes for efficiency.

- In ASML, the leading manufacturer of wafer scanners in the world, an analysis of test processes resulted in recommendations for process improvement, including reordering of tasks to prevent feedback loops and using idle time for scheduling (2009 [E8]).

In Municipality of Heusden, an analysis of the process which handles appeals against the real-estate property valuation or the real-estate property tax (2010 [E5, pg 89]).

Sources to corroborate the impact

[E1] Patent by Fulcrum Microsystems & University of Southern California (US 8495543 B2, US 20110029941 A1, WO 2009155370 A1). http://www.faqs.org/patents/app/20110029941

[E2] Corroboration from Intel Corporation.

[E3] Corroboration from IEEE Task Force on Process Mining.

[E4] Petrify technical Notes: http://www.win.tue.nl/~hverbeek/doku.php?id=projects:prom:plug-ins:conversion:petrify.

[E5] W.M.P. van der Aalst et. al. Process mining: a two-step approach to balance between underfitting and overfitting. Journal of Software and Systems Modeling 9(1): 87-111 (2010).

[E6] W.M.P. van der Aalst. Process mining manifesto: toward real business intelligence. IEEE Computing Now, online: http://www.computer.org/portal/web/computingnow/pmm

[E7] R.S.Mans et.al. (2008). Application of process mining in healthcare - a case study in a Dutch hospital. In: Biomedical Engineering Systems and Technologies (Biostec) 2008, Springer, Communications in Computer and Information Science 25: 425-438.

[E8] Rozinat, A., et. al. (2009) Process mining applied to the test process of wafer scanners in ASML. IEEE Transactions on Systems, Man, and Cybernetics, Part C: Applications and Reviews, vol.39, no.4, pp.474,479, doi: 10.1109/TSMCC.2009.2014169

[E9] Press release on acquisition of Fulcrum by Intel (2011): http://newsroom.intel.com/community/intel_newsroom/blog/2011/07/19/intel-to-acquire-fulcrum-microsystems