A formal foundation for security architecture. Security of computer systems is essential for the maintenance of privacy, confidentiality and integrity of personal, commercial and government data, and the trustworthiness of the computational devices that are embedded in critical societal infrastructure. However, current theoretical understanding of secure systems development is poor. The project will develop our understanding of an emerging approach to the design of secure systems and develop ver ....A formal foundation for security architecture. Security of computer systems is essential for the maintenance of privacy, confidentiality and integrity of personal, commercial and government data, and the trustworthiness of the computational devices that are embedded in critical societal infrastructure. However, current theoretical understanding of secure systems development is poor. The project will develop our understanding of an emerging approach to the design of secure systems and develop verification methods that may be applied to guarantee systems security. Its outcomes will contribute to processes for certifying systems at very high levels of security, a requirement in defence and government settings that will become increasingly significant in the commercial sector.Read moreRead less
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
Integrating a physical and functional genetic map of Prunus dulcis. Genome wide physical mapping is the centrepiece of current genomics research in virtually all plant and animal species. The proposal seeks to champion the development of Prunus dulcis (Rosaceae) as a model perennial species towards parity with other plant model systems for gene discovery and validation. The Rosaceae represents a rich repository of genes of relevance to perenniality, adaptation, sustainable agriculture, health a ....Integrating a physical and functional genetic map of Prunus dulcis. Genome wide physical mapping is the centrepiece of current genomics research in virtually all plant and animal species. The proposal seeks to champion the development of Prunus dulcis (Rosaceae) as a model perennial species towards parity with other plant model systems for gene discovery and validation. The Rosaceae represents a rich repository of genes of relevance to perenniality, adaptation, sustainable agriculture, health and nutrition and the bioindustries. Ultimately, comparative genomics across the family will advance molecular eco-genetics via dissection of traits determining adaptive response. Access to user-friendly molecular markers will also bring greater precision to breeding programmes. Read moreRead less
Biofertiliser technology for improved yields and environmental sustainability of rice and wheat crops. Australia faces the double challenge of improving the efficiency of its crop production while minimising the agricultural impact on its fragile biodiversity. Our project will meet this challenge by providing the technology for using natural biofertilisers in cereal crops. This will reduce our heavy reliance on chemical fertilisers - with associated soil loss, salinity and acidity, and high dema ....Biofertiliser technology for improved yields and environmental sustainability of rice and wheat crops. Australia faces the double challenge of improving the efficiency of its crop production while minimising the agricultural impact on its fragile biodiversity. Our project will meet this challenge by providing the technology for using natural biofertilisers in cereal crops. This will reduce our heavy reliance on chemical fertilisers - with associated soil loss, salinity and acidity, and high demand on scarce water resources - and significantly increase our crop yields. Our advances will help Australian farmers to reduce the costs and increase the productivity of our substantial export crops while improving their environmental sustainability.Read moreRead less
Refinement of Temporal and Epistemic Specifications in Asynchronous Systems. Designing distributed systems is a complex activity requiring rigorous mathematical models of designs and specifications. It is desirable for the mathematical notations to be as close as possible to intuitive notions used by designers. One such notion is the idea that components in a distributed system have states of knowledge. Previous work has developed a calculus enabling derivation of systems with global clock by s ....Refinement of Temporal and Epistemic Specifications in Asynchronous Systems. Designing distributed systems is a complex activity requiring rigorous mathematical models of designs and specifications. It is desirable for the mathematical notations to be as close as possible to intuitive notions used by designers. One such notion is the idea that components in a distributed system have states of knowledge. Previous work has developed a calculus enabling derivation of systems with global clock by series of correctness-preserving transformations from a knowledge-based specification. This project will generalize this work to a calculus for systems that lack a global clock, and implement a tool providing automated support for use of the calculus.Read moreRead less
Regulation of Plant Development by Small RNAs. Understanding the roles of small RNAs and their pathways is a new field of research that is giving, and will continue to give profound insights into how multicellular organisms regulate gene expression at a genomic level. Research in this area has already led to RNA interference technology, by which almost any gene can be switched off, and there is considerable potential for other gene silencing and trait modification technologies to emerge. The pro ....Regulation of Plant Development by Small RNAs. Understanding the roles of small RNAs and their pathways is a new field of research that is giving, and will continue to give profound insights into how multicellular organisms regulate gene expression at a genomic level. Research in this area has already led to RNA interference technology, by which almost any gene can be switched off, and there is considerable potential for other gene silencing and trait modification technologies to emerge. The project will yield insights into fundamental biological processes which are expected to engender applications in agriculture and biotechnology. It will maintain and enhance Australia's position in this area.Read moreRead less
Foundations of Executable Temporal Logic. In many computer applications, including those of temporal reasoning, distributed computations and knowledge representations, the concept of time is of central importance. Multiple granularity of time also plays a critical role as not all events are necessarily defined over a uniform model of time. This project will develop the foundations of executable logical representations, supporting multiple granularity of time. This will allow system developers a ....Foundations of Executable Temporal Logic. In many computer applications, including those of temporal reasoning, distributed computations and knowledge representations, the concept of time is of central importance. Multiple granularity of time also plays a critical role as not all events are necessarily defined over a uniform model of time. This project will develop the foundations of executable logical representations, supporting multiple granularity of time. This will allow system developers access to powerful logical techniques in those applications. In the process, fundamental problems in modelling multiple granularity of time will be identified, and application-independent solutions to those problems will be provided.Read moreRead less
Economical and practical design and analysis of probabilistic distributed systems. Complex computing systems composed of communicating processes are
distributed over networks, and interact with embedded hardware
components. They routinely operate in probabilistic environments:
hardware components fail randomly, but at known rates; and tactical
randomisation resolves competition for resources. Effective
specification, development and analysis methods for these systems
is crucial, and probab ....Economical and practical design and analysis of probabilistic distributed systems. Complex computing systems composed of communicating processes are
distributed over networks, and interact with embedded hardware
components. They routinely operate in probabilistic environments:
hardware components fail randomly, but at known rates; and tactical
randomisation resolves competition for resources. Effective
specification, development and analysis methods for these systems
is crucial, and probability makes that particularly difficult.
The focus of this project is to develop new formal methods that are
economical and practical in use. Exploiting our recent advances in
probabilistic program semantics, we will add probability in a new
way to proven techniques in concurrency theory, including
refinement and hierarchical design.Read moreRead less
Algebraic reasoning for serialisability in probabilistic transaction systems. The ability to analyse complex systems is a vital part of the development of large-scale computer applications; a method that improves the quality of the analysis task would increase the competitiveness of the software industry, would attract future development work (in complex and intelligent systems) to Australia, and could contribute to national security.
The results of this project will have a direct influence ....Algebraic reasoning for serialisability in probabilistic transaction systems. The ability to analyse complex systems is a vital part of the development of large-scale computer applications; a method that improves the quality of the analysis task would increase the competitiveness of the software industry, would attract future development work (in complex and intelligent systems) to Australia, and could contribute to national security.
The results of this project will have a direct influence on currently available design tools; the fact that Australian institutions will be responsible for key theoretical results in this growing field will strengthen Australia's position worldwide as an international centre for computer science.Read moreRead less
Hidden-state modelling for modular analysis of information flow, protection and risk evaluation. Automation is increasing explosively, and the cliche is no longer that there is a cpu chip in your washing machine, television or automobile. Nowadays they are potentially in our cash cards, passports and soon on every item in our shopping baskets. Australia is a leader in adopting and developing such technology.
Security and privacy, hard enough for PCs, thus concerns smaller, more numerous devi ....Hidden-state modelling for modular analysis of information flow, protection and risk evaluation. Automation is increasing explosively, and the cliche is no longer that there is a cpu chip in your washing machine, television or automobile. Nowadays they are potentially in our cash cards, passports and soon on every item in our shopping baskets. Australia is a leader in adopting and developing such technology.
Security and privacy, hard enough for PCs, thus concerns smaller, more numerous devices that we might not even realise we are using.
Our research aims to make it easier and more effective to describe and then successfully build-in features that enforce security without adverse impact on usability.Read moreRead less