 |
The Variety of Variables in Automated Real-Time Refinement
Wildman, L., Fidge, C. and Carrington, D. (2002-11-01) The Variety of Variables in Automated Real-Time Refinement. Technical Report 02-38, Software Verification Research Centre, School of Information Technology, The University of Queensland.
|
|
| |
| Attached Files (Some files may be inaccessible until you login with your UQ eSpace credentials) |
| Name |
Description |
MIMEType |
Size |
Downloads |
svrc_02_38.pdf
|
svrc_02_38.pdf |
application/pdf |
247.99KB |
270 |
svrc_02_38.ps
|
svrc_02_38.ps |
application/postscript |
310.23KB |
66 |
| Author(s) |
Wildman, L.
Fidge, C.
Carrington, D.
|
| Title |
The Variety of Variables in Automated Real-Time Refinement
|
| School, Department or Centre |
Software Verification Research Centre, School of Information Technology
|
| Institution |
The University of Queensland
|
| Report Number |
Technical Report 02-38
|
| Publication date |
2002-11-01
|
| Language |
eng
|
| Subject |
280302 Software Engineering
|
| Abstract/Summary |
The refinement calculus is a well-established theory for deriving program code from specifications. Recent research has extended the theory to handle timing requirements, as well as functional ones, and we have developed an interactive programming tool based on these extensions. Through a number of case studies completed using the tool, this paper explains how the tool helps the programmer by supporting the many forms of variables needed in the theory. These include simple state variables as in the untimed calculus, trace variables that model the evolution of properties over time, auxiliary variables that exist only to support formal reasoning, subroutine parameters, and variables shared between parallel processes.
|
| Keyword(s) |
Computer-aided programming
Program refinement theory
Real-time programming
|
|
|
|
