Embedded software in the transportation sector (railway, automotive and
avionics) needs to meet
high reliability requirements because errors may have severe consequences.
Research since 2008
in the UoA has developed effective reasoning technology to provide
assurance that key error types
are eliminated from embedded software, and has created novel algorithms to
prove its integrity.
Major players such as [text removed for publication] GM and Airbus have
developed in the UoA to verify the absence of errors. A particular
advantage of this technology is
its ability to reason about floating-point arithmetic, meaning that a much
wider class of properties
can be verified. The technology is widely distributed via third party
operating systems and tool-sets.
A spin-out company, Contemplate Ltd, is using advanced static analysis
technology in global top-ten
investment banks and other clients to discover previously undetected
defects in enterprise-scale
business-critical multi-threaded Java codebases. The impact is in terms of
delivered to Contemplate's clients by this technology and in terms of the
formation and growth of
Contemplate as an employer and a successful business.
Graph-theoretic and mathematically rigorous algorithmic methods developed
at the University of Hertfordshire have improved the applicability of
compiler technology and parallel processing. A compiler developed in the
course of a ten-year research programme at the university has been
successfully applied to a number of commercial problems by re-purposing
the research tool. NAG Ltd has adapted the tool into a commercial product
[text removed for publication]. Numerous applications of the mathematical
methods (such as type-flow graphs used conjointly for correctness and
optimisation) have been deployed by industry (including SAP, SCCH, German
Waterways Board) working closely with the university.
Effective industrial design and simulation require efficient and
versatile computing systems. As a result of research performed by our team
experienced in High Performance Computing (HPC), novel software structures
and aligned hardware architectures have led to significant benefits to the
energy supply industry and to microprocessor manufacturers.
As a result of our research with supercomputing, simulation times for
electric field patterns in power components have reduced more than
30-fold, with accurate complex 3-D outputs for an increased range of
configurations, thereby enabling our partner company to achieve results
not possible with commercial software and to reduce product development
costs by $0.5M - $5M p.a.
Our research has been incorporated by Intel into their numerical
libraries and now made available to the general public supported by their
latest processor architectures. Intel now has a 82% share of processors,
according to the November 2013 Top500 list.
Pioneering research into Inductive Logic Programming in the UOA led to the creation of Secerno
Ltd. From 2008 Secerno attracted investment of approximately $20m and successfully released
several updated versions of its product DataWall, based on this Oxford research. In May 2010
Oracle Corporation bought Secerno specifically to gain access to this technology, which now forms
a core part of Oracle's database protection and compliance products. Oracle continues to develop
the software, which is used across the globe by public entities and private companies to protect
databases from internal and external attack and to ensure that they comply with relevant
legislation. Customers include major businesses such as T-Mobile, which uses Database Firewall
to protect 35 million users.
Modern processor architectures (networked multi/many-core nodes),
together with society's expectation of evermore-complex applications,
require fluent mastery of concurrency. To enable this mastery, in the last
two decades our group has taught, researched and developed fundamental
notions of concurrency, new programming languages
(occam-pi, and the KRoC toolset), libraries (JCSP, CCSP, C++CSP,
CHP), runtime systems (the KRoC/CCSP multicore scheduler) and tools
based on formal process algebra (Hoare's CSP, and Milner's pi-calculus).
Our work has had impact in providing new mechanisms for software
development in a number of sectors such as chip design, large-scale
real-time systems, formal interfaces and testing and the space industry.
Testimonials supporting this are available from a variety of industrial
and commercial sources (NXP Semiconductors, Big Bee Consultants, Philips
Healthcare, 4Links Ltd. and Microsoft Research Cambridge). The breadth of
impact of the work is evidenced by download statistics, as well as by
third-party contributions to libraries and documentation.
Work undertaken at the Applied DSP and VLSI Research Group since the
early/mid nineties, has led to a number of significant contributions
underpinning the development and commercial exploitation by industry of
power efficient and complexity reduced integrated Digital Signal
Processing (DSP) systems and products. These developments
have paved the way for a new paradigm in the design of complexity reduced
electronic systems aiding the emergence of numerous new commercial
application areas and products in a diversity of fields. Indeed, these
developments continue their currency and applicability in today's
electronic products sector and thus shall be at the core of this case
The programming languages and systems group at the University of Kent has
built the first comprehensive tools for refactoring functional programs:
HaRe for Haskell, Wrangler for Erlang. These tools not only provide a
large set of refactorings, they also have facilities for managing code
clones and module structure, as well as facilities for users to easily
build their own refactorings.
Programmers in both open source and
commercial projects use the tools to improve their programming and testing
practice, and to restructure existing systems. This improves the quality
of software, reducing bugs/problems for end users and cost for companies;
it thus puts companies at a competitive advantage and improves best
practice in industry. Evidence of take up comes from system downloads,
contributions to open source repositories and company testimonials.
The difficulty of certifying the safety (often termed Verification and
Validation — V&V) of increasingly complex and more autonomous
Guidance, Navigation and Control (GNC) systems is now widely accepted to
be a serious threat to the success of future space missions. In response
to this threat, the European Space Agency has funded Dr Prathyush P Menon
and his team to develop a suite of mathematical tools for the V&V of
advanced GNC systems. These tools have now been widely adopted throughout
the European Space industry, and have been successfully applied by major
companies such as Astrium, Thales-Alenia and GMV to systems ranging from
flexible and autonomous satellites, to launch vehicles and hypersonic
This case study describes the development, application and
commercialisation of an open source tool, BSMBench that enables supercomputer
vendors and computing centres to benchmark their system's
performance. It comprehensively informs the design and testing of new
computing architectures well beyond other benchmarking tools on
the market, such as Linpack.
The significance of our code is that, unlike other benchmarking tools,
it interpolates from a communication- to a computation-dominated
regime simply by varying the (physics) parameters in the code, thus
providing a perfect benchmark suite to test the response of modern
multi-CPU systems along this axis. The impact of this work has great
reach: a start-up company, BSMbench Ltd, has been founded
to develop and commercialise the software; adopters have included IBM
- one of the giants of the supercomputer world (where it uncovered errors
in their compilers); it has been deployed by Fujitsu to validate
its systems, by HPC Wales, a multi-site, commercially focussed national
computer centre and by Transtec, an HPC company employing
over 150 staff; and tutorial articles about BSMBench have appeared
in magazines such as Linux Format.
This software tool spawned from our research into "Beyond the
Standard Model" (BSM) physics which aims to understand the Higgs
mechanism in particle physics at a fundamental level. This involved
simulating quantum field theories using bespoke code on some of the
fastest supercomputers on the planet.