Log in
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 used technology 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 the benefits 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 study.
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 re-entry vehicles.
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.