Understanding concurrent programs using rely-guarantee thinking. Multi-core processors are standard in computers and devices (e.g. smart phones) but much of the software available for these machines is either unreliable or does not exploit the available hardware parallelism. This project will devise techniques for designing concurrent software that exploits these platforms while delivering dependable operation.
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
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
Derivation and timing analysis of concurrent real-time software. Safety-critical computer systems are commonly controlled by concurrent real-time software. Assurance of such systems requires rigorous methods for deriving the software and verifying its logical and timing correctness. This project will directly address this problem via a new paradigm for real-time programming that is based on a machine-independent concurrent real-time programming language, that explicitly represents timing deadlin ....Derivation and timing analysis of concurrent real-time software. Safety-critical computer systems are commonly controlled by concurrent real-time software. Assurance of such systems requires rigorous methods for deriving the software and verifying its logical and timing correctness. This project will directly address this problem via a new paradigm for real-time programming that is based on a machine-independent concurrent real-time programming language, that explicitly represents timing deadlines within programs. This allows a partitioning of the development process into a machine-independent phase that derives a program to meet a high-level specification, and a machine-dependent phase that checks that the timing deadlines within the generated machine code are guaranteed to be met.Read moreRead less
Compilation of Specifications. Computer software now controls critical systems worldwide. International standards require such programs to be produced from mathematically-precise specifications, but the techniques and tools involved are highly complex and unfamiliar to most programmers. This project will show how a tool already used by software developers, the program compiler, can be extended to undertake much of the task automatically. This will be done by devising a compilation strategy, b ....Compilation of Specifications. Computer software now controls critical systems worldwide. International standards require such programs to be produced from mathematically-precise specifications, but the techniques and tools involved are highly complex and unfamiliar to most programmers. This project will show how a tool already used by software developers, the program compiler, can be extended to undertake much of the task automatically. This will be done by devising a compilation strategy, based on program refinement theory, that automatically translates specification statements in programs into executable code. Such an outcome will ultimately improve the speed, accuracy and cost-effectiveness of critical software development.Read moreRead less
Automatic Energy Tuning of Parallel Applications on a Hybrid Supercomputer. Energy efficiency is a critical challenge in building next-generation supercomputers. This project aims to provide a new energy-tuning tool integrated with Cray’s systems, to simplify the process of tuning hybrid applications and managing efficient energy use. Although hardware components play a dominant role in saving energy, heterogeneous systems offer the opportunity to exploit the extremely high concurrency with mode ....Automatic Energy Tuning of Parallel Applications on a Hybrid Supercomputer. Energy efficiency is a critical challenge in building next-generation supercomputers. This project aims to provide a new energy-tuning tool integrated with Cray’s systems, to simplify the process of tuning hybrid applications and managing efficient energy use. Although hardware components play a dominant role in saving energy, heterogeneous systems offer the opportunity to exploit the extremely high concurrency with modest energy consumption using accelerators. Accordingly, the future of parallel computing must consider the trade-off between obtaining the optimal performance and the allowed power budget. The project plans to design parallel programming environments that support energy analysis and tuning.Read moreRead less