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