Log in
Analytical Software Design (ASD), based on Communicating Sequential Processes (CSP) and the Failures Divergences Refinement tool (FDR), has been developed and patented by the specially created Dutch company Verum. The new software, based on research in the UoA, was released in 2009 and has allowed customers to build rigorous, error-free software systems automatically by specifying state machines. ASD, using FDR as its verification engine, has produced many millions of lines of verified code for customers including Philips Medical Systems, Ericsson, FEI and ASML, who typically report at least a 50% reduction in costs and a 90% reduction in errors.
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.
Work conducted at UEL in the area of secure software systems engineering has had impacts on both the private and public sectors, in the UK and abroad. Through its application to financial pre-employment screening it has enabled an award-winning UK company to improve its security processes and become a world leader with respect to secure systems in their sector. This has, in turn, allowed the company to develop a competitive advantage in the market and attract more and larger multinational clients. In the public service sector our work has enabled a Greek governmental department — the National Gazette — to analyse the security implications of fully automating their processes and identify security mechanisms that enhance the security of their new systems. This has improved their service delivery, with significant impacts on Greek society.
Professor Ross Anderson's (University of Cambridge) research in security economics has had considerable impact on public policy and industry practice. Through two reports for ENISA, his work has directly influenced European Commission policy on combatting cyber-crime and on protecting the internet infrastructure. Through his membership of a Blackett Review and appearances before parliamentary committees, he has influenced UK government policy on cyber- security. Personally, and through the positions to which members his research team have moved, his research has influenced a range of organisations, including the US government, the European Union, Google, and Microsoft.