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 application/pdf 239.20KB 2
n02chapter1.pdf n02chapter1.pdf application/pdf 212.56KB 2
n03chapter2.pdf n03chapter2.pdf application/pdf 317.00KB 2
n04chapter3.pdf n04chapter3.pdf application/pdf 313.31KB 3
n05chapter4.pdf n05chapter4.pdf application/pdf 355.04KB 2
n06chapter5.pdf n06chapter5.pdf application/pdf 312.39KB 2
n07chapter6.pdf n07chapter6.pdf application/pdf 302.34KB 2
n08chapter7.pdf n08chapter7.pdf application/pdf 344.50KB 2
n09chapter8.pdf n09chapter8.pdf application/pdf 156.77KB 1
n10appendix.pdf n10appendix.pdf application/pdf 320.69KB 1
n11references.pdf n11references.pdf 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: 98 Abstract Views, 20 File Downloads  -  Detailed Statistics
Created: Fri, 21 Nov 2008, 20:57:41 EST