Research Report - Real-time Systems
In real-time computing, the time at which each output is produced is critical. Producing the right answer too late may be as bad as producing the wrong answer or no answer at all. It is extremely difficult to ensure the correctness of such systems through testing, so rigorous and formal methods are essential in their development. The School in collaboration with the Software Verification Research Centre (SVRC) has established a substantial team to undertake research into methods and tools for development of verified real- time programs. This work is primarily funded through external grants from the Australian Research Council.
In practice, embedded real-time systems comprise numerous interacting components. An ARC-funded project is applying real-time formal methods to the specification of distinct system components, and is defining compositional operators that allow these specifications to be combined. Modelling component-based systems is made easier by using an ‘object oriented’ formalism. Ongoing research is showing how the Object-Z specification notation can be upgraded to handle real-time requirements.
Programming real-time systems is difficult because many timing requirements cannot be expressed using the statements provided in contemporary programming languages. This project is devising simple extensions to programming languages for expressing timing requirements, and is showing how these new features can be formally defined, introduced and analysed. A major part of this research is development of a theory for extracting verifiable timing constraints from real-time programs. This will allow conversion of timing requirements expressed by a high-level language programmer into a form that can be automatically verified by a simple execution time analyser for assembler language code.
While model checking has been suggested as a means of reasoning about software, its application is limited since software specifications (as opposed to digital hardware specifications for which model checking was originally developed) tend to be too complex. One approach to overcoming this problem is to use a theorem prover to perform property-preserving simplifications of the specification (abstraction) or to partition the specification, and model checking problem, into simpler parts (decomposition). A project is developing such techniques for Real-Time Object-Z specifications.
Associated Staff
A/Prof David Carrington
Prof Ian Hayes
Prof Peter Lindsay
Dr Paul Strooper
A/Prof John Yesberg
<%@ include file="/include/footer.inc.jsp" %>