Go backward to Proof of Fairness
Go up to Top
Go forward to Formal Specification
Hiding Variables
- A simple processor/memory interface:
- Processor issues read and write operations executed by
memory.
- Three interface registers:
- op: set by processor to indicate operation, reset by memory after
operation.
- adr set by processor to indicate memory address to be read or
written.
- val set by processor to indicate value to be written, set by
memory to return result of read.
- Specification Phi:
- memory() current value of location .
- Address set of legal address.
- MemVal set of possible memory values.
- Action A(,) assignment memory():=v.
- Processor actions R, W.
- Memory responses R, W.
Wolfgang.Schreiner@risc.uni-linz.ac.at
Id: tla2.tex,v 1.2 96/05/06 10:48:53 schreine Exp Locker: schreine