The Specification and Refinement of Timed Processes

Mahony, Brendan Patrick (1992). The Specification and Refinement of Timed Processes PhD Thesis, , University of Queensland.

       
Attached Files (Some files may be inaccessible until you login with your UQ eSpace credentials)
Name Description MIMEType Size Downloads
n01front.pdf n01front.pdf Click to show the corresponding preview/stream application/pdf 239.20KB 2
n02chapter1.pdf n02chapter1.pdf Click to show the corresponding preview/stream application/pdf 212.56KB 2
n03chapter2.pdf n03chapter2.pdf Click to show the corresponding preview/stream application/pdf 317.00KB 2
n04chapter3.pdf n04chapter3.pdf Click to show the corresponding preview/stream application/pdf 313.31KB 3
n05chapter4.pdf n05chapter4.pdf Click to show the corresponding preview/stream application/pdf 355.04KB 2
n06chapter5.pdf n06chapter5.pdf Click to show the corresponding preview/stream application/pdf 312.39KB 2
n07chapter6.pdf n07chapter6.pdf Click to show the corresponding preview/stream application/pdf 302.34KB 2
n08chapter7.pdf n08chapter7.pdf Click to show the corresponding preview/stream application/pdf 344.50KB 2
n09chapter8.pdf n09chapter8.pdf Click to show the corresponding preview/stream application/pdf 156.77KB 1
n10appendix.pdf n10appendix.pdf Click to show the corresponding preview/stream application/pdf 320.69KB 1
n11references.pdf n11references.pdf Click to show the corresponding preview/stream application/pdf 215.38KB 1
Author Mahony, Brendan Patrick
Thesis Title The Specification and Refinement of Timed Processes
Institution University of Queensland
Publication date 1992
Thesis type PhD Thesis
Supervisor Dr Ian Hayes
Abstract/Summary The use of predicate transformers to model the action of sequential programs has allowed the construction of a refinement calculus for expressing the formal verification of the top-down development of sequential programs. It is shown that predicate transformers may also be used to model real-time processes. The notions of precondition and postcondition in the sequential refinement calculus are replaced by the notions of assumption and effect. In this way the formal development of real-time processes may also be expressed within the refinement calculus. Notations are developed for the specification and implementation of real-time processes within the framework of the refinement calculus. Several case-studies are presented to demonstrate the utility of this approach.
Keyword predicate transformers
formal verification
sequential programs

 
Citation counts: Google Scholar Search Google Scholar
Access Statistics: 132 Abstract Views, 20 File Downloads  -  Detailed Statistics
Created: Fri, 21 Nov 2008, 20:57:41 EST