Implementing Feferman-Landin Logic. The objective of this project is to utilise computer based verification tools (such as PVS and Rewritting Logic) to develop a software engineering environment for specifying and verifying systems written in high-level programming languages such as Java, Scheme, and ML. The project will thus subtantially advance the use of formal computer based tools to develop reliable programs and specifications for life-critical systems. The project will also develop form ....Implementing Feferman-Landin Logic. The objective of this project is to utilise computer based verification tools (such as PVS and Rewritting Logic) to develop a software engineering environment for specifying and verifying systems written in high-level programming languages such as Java, Scheme, and ML. The project will thus subtantially advance the use of formal computer based tools to develop reliable programs and specifications for life-critical systems. The project will also develop formally
based interoperability between the PVS and Maude systems, two widely
used computer tools for reasoning about complex systems.Read moreRead less
Early detection of component incompatibility in time-dependent computer architectures. Complex real-time systems are increasingly being built by integrating off-the-shelf components. There are obvious benefits to this approach, but the hidden costs associated with integration are still a major problem. Our proposed approach will enable early detection of integration problems, and thus provide potential for large cost savings. This brings with it clear benefits to industry. One industry that woul ....Early detection of component incompatibility in time-dependent computer architectures. Complex real-time systems are increasingly being built by integrating off-the-shelf components. There are obvious benefits to this approach, but the hidden costs associated with integration are still a major problem. Our proposed approach will enable early detection of integration problems, and thus provide potential for large cost savings. This brings with it clear benefits to industry. One industry that would benefit by such technology is the Australian Navy, which is increasingly being confronted with the challenge of integrating off-the-shelf components in large Naval Combat Systems. Read moreRead less
Making software more reliable using a new model for entropies of computers' internal state. A new mathematical analysis of the way computer systems exchange data between their components has led to novel design approaches for the programs implementing those systems. This reduces their cost and increases their reliability, with improvements ranging from small-scale smart devices to widely distributed internet protocols.
Automation of metric temporal reasoning. A major contemporary engineering concern is to ensure the predictable and robust operation of computer systems involving software, hardware, and human users. The need for systematic and careful construction of such systems requires the development of formal methods based on a dense view of time rather than the traditional step-by-step models.
Machine-checked Foundations for Verified Vote Counting. The project will deliver a general methodology for developing formal logical specifications of the Acts of Parliament for many common systems for counting votes in preferential elections. The project will deliver corresponding computer programs to count votes according to these systems and will deliver formal independently checkable proofs that the programs meet their specification. Such formally verified computer programs provide a legally ....Machine-checked Foundations for Verified Vote Counting. The project will deliver a general methodology for developing formal logical specifications of the Acts of Parliament for many common systems for counting votes in preferential elections. The project will deliver corresponding computer programs to count votes according to these systems and will deliver formal independently checkable proofs that the programs meet their specification. Such formally verified computer programs provide a legally sound basis for counting votes by computer. The methodology will also allow electoral commissioners to improve the natural language descriptions of the relevant Acts of Parliament which are often woefully out of date with current practice.Read moreRead less
automated strategic reasoning. Formal methods are used to ensure robust correct behaviour in design and implementation of computer systems. Traditional models of computer operation involve a linear sequence of behaviour but today’s systems are complex interactions between many components including the environment of the system and human users. Thus analysis is done via a logical game between components where each is trying to meet its specified requirements regardless of what others do: formalis ....automated strategic reasoning. Formal methods are used to ensure robust correct behaviour in design and implementation of computer systems. Traditional models of computer operation involve a linear sequence of behaviour but today’s systems are complex interactions between many components including the environment of the system and human users. Thus analysis is done via a logical game between components where each is trying to meet its specified requirements regardless of what others do: formalisms include branching time and competing coalitions of agents. This project is to take early advantage of recent breakthroughs in automated logical reasoning with such models by the investigator to deliver general practical techniques of system development and verification.Read moreRead less
More information for better utility; less information for better privacy. More information for better utility; less information for better privacy. The contradiction is everywhere in contemporary IT: doctors need accurate information for diagnosis, but insurance companies' access should be limited; on-line retailers use your postcode to present interesting products, but they also deduce from it how much you will pay. One way to manage this contradiction is to tolerate "small" information flows p ....More information for better utility; less information for better privacy. More information for better utility; less information for better privacy. The contradiction is everywhere in contemporary IT: doctors need accurate information for diagnosis, but insurance companies' access should be limited; on-line retailers use your postcode to present interesting products, but they also deduce from it how much you will pay. One way to manage this contradiction is to tolerate "small" information flows providing the risks involved can be accurately gauged. This project will build on recent advances in information measuring to develop new techniques for measuring the extent to which computer systems can defend against threats to privacy. Success in this project will lead to completely novel methods for security analysis of on-line applications where privacy is a critical issue.Read moreRead less
Building correct-by-construction distributed systems from specifications stating how agents' knowledge evolves over time. Many distributed computer system implementations fail to comply with their original informal requirement specification. These requirements typically refer to the migration of information through the system over time, but current specification languages are not rich enough to express such requirements on a sufficiently abstract level. This results in a huge error-provoking gap ....Building correct-by-construction distributed systems from specifications stating how agents' knowledge evolves over time. Many distributed computer system implementations fail to comply with their original informal requirement specification. These requirements typically refer to the migration of information through the system over time, but current specification languages are not rich enough to express such requirements on a sufficiently abstract level. This results in a huge error-provoking gap between the informal requirements and the starting point of formally verifiable development. To minimise this gap, we develop a particularly expressive specification language, a calculus for stepwise refinement from such specifications down to distributed systems, and an automated tool for checking and supporting refinement steps in the calculus.Read moreRead less