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
Verified Emulation of Legacy Mission Computer Systems. Processor obsolescence is a serious maintenance problem for long-lived computer control systems in military aircraft and other critical applications. A promising solution is to interpose an emulator program between the original "legacy" software and a replacement processor. Unfortunately, no techniques exist for accurately verifying that this procedure preserves the original system's functional and timing behaviour. A particular challenge ....Verified Emulation of Legacy Mission Computer Systems. Processor obsolescence is a serious maintenance problem for long-lived computer control systems in military aircraft and other critical applications. A promising solution is to interpose an emulator program between the original "legacy" software and a replacement processor. Unfortunately, no techniques exist for accurately verifying that this procedure preserves the original system's functional and timing behaviour. A particular challenge is that processor emulations involve both legacy code and new subroutines, written in different programming languages. This project will enable verification of safety and mission-critical emulated systems by devising a multilingual modelling and reasoning formalism, based on program refinement theory.Read moreRead less
Adapting the Bulk Synchronous Parallel processing model to Peer-to-Peer Networked Computing. Advances in distributed computing have shown that data parallel and parametric applications domains are amenable to wide area distribution. The project will advance the Bulk Synchronous Parallel processing model to describe innovative applications from the loosely synchronous domain, e.g. fluid dynamics, strategy algorithms and N-body problems are challenges that have significant scientific and industria ....Adapting the Bulk Synchronous Parallel processing model to Peer-to-Peer Networked Computing. Advances in distributed computing have shown that data parallel and parametric applications domains are amenable to wide area distribution. The project will advance the Bulk Synchronous Parallel processing model to describe innovative applications from the loosely synchronous domain, e.g. fluid dynamics, strategy algorithms and N-body problems are challenges that have significant scientific and industrial value. The project specializes the exciting peer-to-peer paradigm, a frontier of inter-networking technology. By using the latest techniques and taking advantage of the technology implosion caused by low cost parallel infrastructure, the project outcomes will give Australia a strong position in the future of parallel technology.Read moreRead less
Towards High-performance and Fault-tolerant Distributed Java Implementations. Java Virtual Machines form an important part of the web and business
server market. Distributed Java Virtual Machines have the potential to
make a significant contribution to industries that utilize this
technology. An attractive platform for this purpose is the
cluster, a highly cost-effective and scalable parallel computer
model. However, realizing on such a platform a high performance virtual
machine implem ....Towards High-performance and Fault-tolerant Distributed Java Implementations. Java Virtual Machines form an important part of the web and business
server market. Distributed Java Virtual Machines have the potential to
make a significant contribution to industries that utilize this
technology. An attractive platform for this purpose is the
cluster, a highly cost-effective and scalable parallel computer
model. However, realizing on such a platform a high performance virtual
machine implementation tolerant to hardware and software faults, and
having efficient memory utilization, presents many challenging research
issues. This project will address these issues by extending a highly
efficient and extensible Java implementation to be aware of its cluster
environment.
Read moreRead less
Analysis of two-phase effects in sloshing of liquids in marine tanks. One of the winners in the current greenhouse debate is natural gas, and the global market will see the need for transporting large volumes of LNG. Australia's North West Shelf is one of the largest offshore gas reserves in the world. The gas market is one of the biggest contributors for the country's economy. Australia leads the world in the use of tankers for transport of Liquefied Natural Gas (LNG). However, consistent re ....Analysis of two-phase effects in sloshing of liquids in marine tanks. One of the winners in the current greenhouse debate is natural gas, and the global market will see the need for transporting large volumes of LNG. Australia's North West Shelf is one of the largest offshore gas reserves in the world. The gas market is one of the biggest contributors for the country's economy. Australia leads the world in the use of tankers for transport of Liquefied Natural Gas (LNG). However, consistent research in LNG is lacking. This research is a fundamental inquiry into the physics of liquid sloshing and the importance of two-phase effects on sloshing. The research can provide answers that ensure safe operation and transport of LNG from Australia.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
Redesigning Typesetting for the Digital Age: Multilingual Layout on Multiple Media. We propose to create and develop a new model for character-level automatic typesetting, much more flexible than existing approaches. This model will support quality typesetting of all of the modern - and many ancient - languages and scripts, on media such as paper, computer screen, paper maps and online maps, for regular and safety-critical applications.
The fundamental innovations in this proposal are the us ....Redesigning Typesetting for the Digital Age: Multilingual Layout on Multiple Media. We propose to create and develop a new model for character-level automatic typesetting, much more flexible than existing approaches. This model will support quality typesetting of all of the modern - and many ancient - languages and scripts, on media such as paper, computer screen, paper maps and online maps, for regular and safety-critical applications.
The fundamental innovations in this proposal are the use of a tree-structured parameter space (generalization of Unix environment variables) and a multiple-pass approach to typesetting (as used in compilers). These innovative techniques will be integrated into computer software used worldwide.Read moreRead less
Combining Time Bands and Teleo-Reactive Programs for Advanced Dependable Real-Time Systems. Society is becoming increasingly reliant on sophisticated real-time computer systems in applications ranging from car stability control to critical infrastructure, such as railway signalling systems. Further, there is a demand for ever greater automation and sophistication in the software controlling these systems. The research challenge in this project is to provide robust implementations of these system ....Combining Time Bands and Teleo-Reactive Programs for Advanced Dependable Real-Time Systems. Society is becoming increasingly reliant on sophisticated real-time computer systems in applications ranging from car stability control to critical infrastructure, such as railway signalling systems. Further, there is a demand for ever greater automation and sophistication in the software controlling these systems. The research challenge in this project is to provide robust implementations of these systems in a way that allows one assess their dependability.
Australia industry is actively working in these areas through companies like Ansaldo Australia, in automated railway systems, and Boeing Australia, in the defence sector.Read moreRead less
A Unified Grid Programming Methodology for Global e-Science. This project will contribute to the national benefit in three important ways. First, we will build a set of novel e-Science applications as demonstrator projects in areas of national priority. These will have enormous economic impact in areas ranging from environmental management to health. Second, we will build software infrastructure that will have both commercial and strategic value in its own right. Third, we shall build a critical ....A Unified Grid Programming Methodology for Global e-Science. This project will contribute to the national benefit in three important ways. First, we will build a set of novel e-Science applications as demonstrator projects in areas of national priority. These will have enormous economic impact in areas ranging from environmental management to health. Second, we will build software infrastructure that will have both commercial and strategic value in its own right. Third, we shall build a critical mass of expertise that bridges the physical sciences and computer science. The support provided to this proposal will allow multi-disciplinary teams to address scientific problems of significant scale.Read moreRead less
Analysing model transformations for combinatorial problems. Maximising the benefits of limited resources is crucial for our industry, our hospitals, our security and our environment. This is achievable through a technology called combinatorial optimisation, which also supports wiser investment, better engineering, and even accelerated bio-informatics. Applying the technology is highly skilled and effort intensive, so most of its potential benefits are unrealised. This project will break down ....Analysing model transformations for combinatorial problems. Maximising the benefits of limited resources is crucial for our industry, our hospitals, our security and our environment. This is achievable through a technology called combinatorial optimisation, which also supports wiser investment, better engineering, and even accelerated bio-informatics. Applying the technology is highly skilled and effort intensive, so most of its potential benefits are unrealised. This project will break down some of the barriers which make it hard to use. The ultimate goal is to let the user state the problem in simple terms, and the computer work out how best to solve it. Our vision is for groups and organisations large and small to reap the benefits of combinatorial optimisation.Read moreRead less