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.
| Identifer | oai:union.ndltd.org:ADTP/253798 |
| Creators | Mahony, Brendan Patrick |
| Source Sets | Australiasian Digital Theses Program |
| Detected Language | English |
Page generated in 0.1548 seconds