Design and Formal Verification of Control and Data Acquisition Protocols. This research will develop new specification and verification techniques for remote control protocols, used among interconnected sites in supply utilities such as electricity grids, based on a proven formal methods technology. These protocols are used in the monitoring of data from remote sites, and the transmission of control commands to such sites from a central location. Benefits to the industrial partner include increa ....Design and Formal Verification of Control and Data Acquisition Protocols. This research will develop new specification and verification techniques for remote control protocols, used among interconnected sites in supply utilities such as electricity grids, based on a proven formal methods technology. These protocols are used in the monitoring of data from remote sites, and the transmission of control commands to such sites from a central location. Benefits to the industrial partner include increased assurance that their control technology does correctly realise the adopted protocols. Assurance of correctness is significant in that incorrect protocol implementation may cause errant operation of equipment, and lead to economic and environmental damage.Read moreRead less
Automatic software verification: harnessing constraint technologies. As we come to rely on software to manage more and more aspects of our lives, the importance of software reliability increases; yet as programs become increasingly complex, reliability becomes ever more elusive. This project will develop automated tools and techniques to ensure that programs do what they were intended to do.
Analysing Computer Arithmetic to Improve Software Reliability. Most computer programs deal with integers. Automated tools designed to verify the correct behaviour of software usually assume the software deals with idealised mathematical integers, since this simplifies reasoning significantly. In reality, most programs work with integer number representations that approximate the ideal. This compromises the soundness of many verification tools. This project will design sound reasoning tools that ....Analysing Computer Arithmetic to Improve Software Reliability. Most computer programs deal with integers. Automated tools designed to verify the correct behaviour of software usually assume the software deals with idealised mathematical integers, since this simplifies reasoning significantly. In reality, most programs work with integer number representations that approximate the ideal. This compromises the soundness of many verification tools. This project will design sound reasoning tools that are aware of the true nature of computer integer arithmetic.Read moreRead less
An extensible framework for analysis of Java language-based security conformance. Java is a programming language and platform running on 3 billion devices. While Java provides a sandbox-based security architecture within the Java Class Library to protect systems from untrusted code downloaded from Internet, it cannot defend against implementation bugs that occur in the Java Class Library. The goal of this project is to provide a formal model of the Java security architecture, which can be used b ....An extensible framework for analysis of Java language-based security conformance. Java is a programming language and platform running on 3 billion devices. While Java provides a sandbox-based security architecture within the Java Class Library to protect systems from untrusted code downloaded from Internet, it cannot defend against implementation bugs that occur in the Java Class Library. The goal of this project is to provide a formal model of the Java security architecture, which can be used by program analysers to identify faulty or insufficient security checks in the Java Class Library that may lead to the sandbox being bypassed.Read moreRead less
RichProlog, a System for Deducing, Inducing and Learning in the Declarative Programming Paradigm. The aim of the project is to contribute to bridge the gap between learning and logic, theoretically and practically. Our purpose is to extend considerably the scope of the declarative programming paradigm, and build a system that can be used to solve learning or discovery problems as encountered in Artificial Intelligence. The system will enable rapid prototyping when applied to problems involving d ....RichProlog, a System for Deducing, Inducing and Learning in the Declarative Programming Paradigm. The aim of the project is to contribute to bridge the gap between learning and logic, theoretically and practically. Our purpose is to extend considerably the scope of the declarative programming paradigm, and build a system that can be used to solve learning or discovery problems as encountered in Artificial Intelligence. The system will enable rapid prototyping when applied to problems involving deduction, induction, and nonmonotonic reasoning. We intend the system to become a standard tool for tackling a broad range of applications, and the underlying theory to provide new insights on the logical foundations of Artificial Intelligence.
Read moreRead less
Design and verification of correct, efficient and secure concurrent systems. This project aims to provide methods for the design and verification of correct, secure and efficient concurrent software that are scalable and mechanised. Computers with multiple processors are now the norm and are used in a wide range of safety, security and mission critical software applications such as transport, health and infrastructure. These multi-core architectures have the potential to lead to important effici ....Design and verification of correct, efficient and secure concurrent systems. This project aims to provide methods for the design and verification of correct, secure and efficient concurrent software that are scalable and mechanised. Computers with multiple processors are now the norm and are used in a wide range of safety, security and mission critical software applications such as transport, health and infrastructure. These multi-core architectures have the potential to lead to important efficiency gains, but can introduce complex and error-prone behaviours that cannot be managed using traditional software development approaches. This project will produce better, scalable and mechanised methods for the design and verification of such software which is expected to reduce the prevalence of failures in efficient, modern software.Read moreRead less
Simulation and verification of system-level specifications of requirements and constraints using Rosetta. Modern computer-based systems comprise a mixture of electronic hardware and embedded computer software that interacts with mechanical and other non-electrical subsystems. Future design capability will depend on being able to model the requirements and constraints of heterogeneous systems, so that they can be simulated and formally verified before being manufactured and deployed. This project ....Simulation and verification of system-level specifications of requirements and constraints using Rosetta. Modern computer-based systems comprise a mixture of electronic hardware and embedded computer software that interacts with mechanical and other non-electrical subsystems. Future design capability will depend on being able to model the requirements and constraints of heterogeneous systems, so that they can be simulated and formally verified before being manufactured and deployed. This project will develop techniques and software tools for simulation and verification based on the new Rosetta system-level design language. These tools will make the design of complex computer-based systems faster, more reliable and less costly by minimizing design errors early in the design flow.Read moreRead less
Provable elimination of information leakage through timing channels. This project aims to develop techniques to solve the issue in information security of unauthorised information flow resulting from competition for shared hardware resources. The project will combine operating systems design, formal hardware models, information-flow reasoning and theorem proving to achieve a goal that is widely considered infeasible. The project is expected to result in a system that prevents leakage of critical ....Provable elimination of information leakage through timing channels. This project aims to develop techniques to solve the issue in information security of unauthorised information flow resulting from competition for shared hardware resources. The project will combine operating systems design, formal hardware models, information-flow reasoning and theorem proving to achieve a goal that is widely considered infeasible. The project is expected to result in a system that prevents leakage of critical information, such as encryption keys, through timing channels. This should prevent sophisticated attacks on public clouds, mobile devices and military-grade cross-domain devices.Read moreRead less
Evolutionary multi-objective algorithms for Global Grids. This research investigates alternative software technologies for Grid-based evolutionary multi-objective decision algorithms. By employing the latest adaptive techniques and taking advantage of the low cost Grid infrastructure, new parallel evolutionary systems will be developed that can rapidly supply robust solutions to complex problems. This project will further develop an understanding of scaling issues in parallel evolutionary syste ....Evolutionary multi-objective algorithms for Global Grids. This research investigates alternative software technologies for Grid-based evolutionary multi-objective decision algorithms. By employing the latest adaptive techniques and taking advantage of the low cost Grid infrastructure, new parallel evolutionary systems will be developed that can rapidly supply robust solutions to complex problems. This project will further develop an understanding of scaling issues in parallel evolutionary systems and pave the way for even more widespread application of evolutionary techniques for large scale, data-intensive applications in science and industry.Read moreRead less
Intelligent Model Checking. Real-world systems are typically so complex that software engineers require specialised CAD tools to debug and verify a design. Model checking is a formal method that is used extensively for this purpose, particularly for mission-critical systems. In this work, a new kind of verifying tool, based on model checking, is developed. This new model checker is intelligent because a heuristic search is integrated into the underlying formalism. It is not exhaustive, and is mo ....Intelligent Model Checking. Real-world systems are typically so complex that software engineers require specialised CAD tools to debug and verify a design. Model checking is a formal method that is used extensively for this purpose, particularly for mission-critical systems. In this work, a new kind of verifying tool, based on model checking, is developed. This new model checker is intelligent because a heuristic search is integrated into the underlying formalism. It is not exhaustive, and is more efficient than a traditional model checker during the design phase because it does only a minimum amount of work in its search for a fault.Read moreRead less