Research Report - 2001
Real-Time Systems
Academic Staff
A/Prof Ian Hayes
A/Prof David Carrington
Research Staff
Dr Colin Fidge (SVRC)
Mr Luke Wildman (SVRC)
Dr Graeme Smith (SVRC)
Dr Karl Lermer (SVRC)
Research Students
Mr Steven Grundon
Contact Details
A/Prof Ian Hayes
Email: ianh@csee.uq.edu.au
Tel: 3365 2386
A/Prof David Carrington
Email: davec@csee.uq.edu.au
Tel: 3365 3310
Webpages
www.svrc.it.uq.edu.au
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 Department in collaboration with the Software Verfication 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.
A Real-Time Program Refinement Tool
Tool support is essential to cost-effective development of verified programs. This project devised a prototype “refinement tool” for formal development of programs with strict timing constraints. The tool combined real-time refinement rules with window-inference based reasoning. The project was funded by the Australian Research Council and successfully concluded in December 2000. The real-time tool extends the SVRC's Program Refinement Tool (PRT) with additional contextual information, new operators, and new program development rules. PRT is itself built on the SVRC’s Ergo theorem prover. Several improvements were made to the tool throughout 2000, including a significant upgrade to use a newer version of Ergo. Motivated by ongoing case studies, the capabilities of the tool were recently extended even further. To accommodate applications involving concurrency, formal development rules were devised for introducing the concurrent programming operators “parallel”, “pipe” and “feedback”. These were then implemented in the tool and exercised on a case study based on the data sampling component of an embedded controller. In related work, SVRC investigations into other forms of real-time tool support continue, especially the application of a commercial simulation tool for modelling multi-tasking systems.
L. Wildman, C. J. Fidge and D. Carrington. Computer-Aided Development of a Real-Time Program.
J. Shield, I. Hayes and D. Carrington. Mechanising the Reals in an Interactive Theorem Prover using Theory Interpretation.
A.P. Martin and C.J. Fidge. Lifting in Z.
A. de Beer and C.J. Fidge. A Simple Multi-Tasking Simulator.
A Component-Oriented Real-Time Formalism
In practice, embedded real-time systems comprise numerous interacting components. This 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. Significant progress continues to be made on a comprehensive refinement calculus for development of sequential real-time program code. This research has now achieved a significant level of maturity. Recent improvements have focussed on the role of time-invariant assertions and “deadline” statements for reasoning about real-time code. To support concurrency, a new parallel composition operator for specifications was developed. Unlike previous definitions, it accurately models the potential negative impact of a malfunctioning system component on other components. 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. Progress also continues on the “realization” process for systematically transforming specifications. In particular, a significant case study was completed showing how realization steps can be interleaved with traditional refinement ones, in order to incrementally introduce component-specific detail to an evolving system design. This cost-saving approach avoids the need to redo development steps when system requirements change.
G. Smith. Stepwise Development from Ideal Specifications.
I.J. Hayes. Reasoning about Real-Time Programs Using Idle-Invariant Assertions.
G. Smith and C. Fidge. Incremental Development of Real-Time Requirements: The Light Control Case Study.
I.J. Hayes. Using Deadline Commands to Reason about Non-Terminating Loops.
I.J. Hayes and M. Utting. A Sequential Real-Time Refinement Calculus.
G. Smith and I. Hayes. Structuring Real-Time Object-Z Specifications.
G. Smith. Recursive Schema Definitions in Object-Z.
Analysis of Real-Time Programs
Programming a real-time system is difficult because many timing requirements can not be expressed using the statements provided in contemporary programming languages. This ARC-funded 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. Long-term research into formal laws for deriving assembler code from real-time programs was recently completed. This work provides a formal basis for modelling the code generation strategies used by high-level language compilers. This is important because some safety standards require that programs are developed using verified or trustworthy compilers. A major area of research is development of an algorithm for automatically 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 checked by a simple execution time analyser for assembler language code. Initial experiments have been undertaken with a prototype version of the algorithm. Other recent research showed how formal development of real-time programs can be facilitated by using temporary “auxiliary” variables that model significant properties, but have no existence in the final machine code.
K. Lermer and C. J. Fidge. A Formal Model of Real-Time Program Compilation.
K. Lermer and P. Strooper. Refinement and State Machine Abstraction.
I. J. Hayes. Real-Time Program Refinement using Auxiliary Variables.
<%-- end content --%><%@ include file="/include/footer.inc.jsp" %>