Log in
QinetiQ's Systems Assurance Group (SAG) collaborated with the UoA from the early 1990s on the use of their research, such as Communicating Sequential Processes (CSP) and the verification tool FDR. SAG applied these to MOD projects, assessing the dependability of software systems, such as Plug & Play Weapons architectures and Eurofighter avionics, up until 2012. In 2012, core people from SAG set up the company D-RisQ. D-RisQ obtained a license from QinetiQ enabling them to take the UoA's technology forward and commercialise it. The core of this impact relates to safety-case analysis for legacy systems.
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.
The research work undertaken at Middlesex University on model checking for multi-agent systems has made a significant contribution both to theory and to applications for the verification of complex and critical systems, such as autonomous rovers and avionic scenarios. These scenarios require the verification of properties that go beyond traditional temporal requirements and include epistemic and strategic modalities. Our work has contributed to the development of efficient model checking algorithms and tools that implement state-of-the art features; both the algorithms and the tools have been applied to a number of real-life instances, including scenarios from NASA applications.
Bath research on the design of multi-agent software systems governed by norms and institutions has directly influenced the development of the essential business systems of an internet-based trading company, and been instrumental in their success.
The Book Depository (BD) was founded in 2004. In 2005, their Chief Technical Officer, Emad Eldeen Elakehal, sought the expertise of Julian Padget in the Department of Computer Science at Bath, and began a part-time PhD, working on the application of normative frameworks to the design and implementation of business systems. Elakehal has applied these principles in the design and construction of two key subsystems of BD's software infrastructure: the catalogue maintenance system (live since 2006) and the price checker and setter system (since 2008). Their effectiveness has underpinned the growth and success of the company by providing robust software implementation of business processes that adapt to changing market conditions. The company's turnover grew from £24M to £120M from 2008 - 2011, and continues to grow. The software systems enabled this growth to take place with no increase in the operations team's manpower, and now handle a catalogue of over 8 million titles, from 120 suppliers, all available within 48 hours to customers on the Book Depository's own web site or via Amazon's marketplace: all Amazon book customers have seen offers of books generated by this software. The software underpins BD's award-winning business, a unique offering in the book retail sector which attracted takeover by Amazon in 2011. BD's Managing Director states that "without the agent/norm based technical systems not one of the business' USPs could have been effectively realised."
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.
Research into the operational characteristics and applicability of biological reaction networks, carried out at the university in collaboration with groups at Caltech and Sony Systems, revealed the pressing need for a standard format that could be used for storage and exchange of mathematical models of such systems. Hertfordshire researchers played a crucial role in the initial design, dissemination and early exploitation of the Systems Biology Markup Language, SBML, now recognised as the de facto standard format for this purpose. Several major scientific publishers operating across academic boundaries require their authors to use SBML, and 254 software tools, including MATLAB and Mathematica, are now SBML-compliant. Online forums testify to a sizeable, international user-developer community that encompasses engineers, biologists, mathematicians and software developers.
The spin-out company CSM Ltd. was set up in 1991 to commercially develop Durham research on program transformation. Up until 1999, this company (which in the mid-90's became Durham Software Engineering Ltd. and subsequently Software Migrations Ltd.) and researchers at Durham University developed the FermaT Workbench: an industrial-strength assembler re-engineering workbench for program comprehension, migration and re-engineering. In 1999, Software Migrations Ltd. relocated to St. Albans and now has an extensive list of national and international clients. All its products (software and services) are built on the FermaT Workbench and has generated considerable revenue with this revenue strongly expected to rise steeply in the near future.
This case is based on economic impact. It shows how research by Professor Michael Wooldridge at the University of Liverpool on the Gaia Methodology for agent-oriented software engineering improved the performance of the Swiss company Whitestein Technologies AG and of international users of its key product. Specifically, the research enabled Whitestein to develop its business process management system (BPM) Living Systems Process Suite which delivers several million pounds per year of revenues, corresponding to 50% of their total business revenues. Users of Whitestein's Living Systems Process Suite since 2008 include Daimler AG, Transcor Astra Group, Vienna Insurance Group, and the US Department of Veterans Affairs. In 2010 Gartner, the world's leading IT advisory company, recognized the impact and innovation of the Living Systems Process Suite by naming Whitestein a Cool Vendor in BPM.
A series of econometric methods and software, designed by a team of econometricians at Oxford, have been adopted as standard by a large range of governmental bodies, international agencies and businesses. The econometric methods are designed to model and forecast high-dimensional, evolving economic processes facing multiple structural shifts, while the econometric software (PcGive) implements the resulting best-practice procedures. The application of these methods have resulted in more appropriate empirical models, improved robust forecasts, and, consequently, better decision making by these bodies.
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.