Mallon, W.C. (1995) Contraction based proof methods for a delay-insensitive algebra. Master's Thesis / Essay, Computing Science.
|
Text
Infor_Ma_1995_WCMallon.CV.pdf - Published Version Download (647kB) | Preview |
Abstract
We define a metric for delay insensitive processes. We derive metric properties of operators in a delay insensitive algebra, and use these properties to formalize the notion of "input guardedness".We also derive a method to verify whether a function composed of operators is contracting with regard to its process arguments. We define two relations on processes, and use these relations to derive proof methods for proving equality and refinement. Both proof methods can be used in linear derivations. We present the proof methods in a simple format, that can easily be implemented in proof verification tools. We give an example of the proof method for proving equality by the derivation of a component based design of an n-place delay-insensitive buffer.
| Item Type: | Thesis (Master's Thesis / Essay) |
|---|---|
| Degree programme: | Computing Science |
| Thesis type: | Master's Thesis / Essay |
| Language: | English |
| Date Deposited: | 15 Feb 2018 07:29 |
| Last Modified: | 15 Feb 2018 07:29 |
| URI: | https://fse.studenttheses.ub.rug.nl/id/eprint/8786 |
Actions (login required)
 |
View Item |