Quellcode-Bibliothek README.txt

Author: John Fitzgerald and Peter Gorm Larsen


The tracker example is used in the mapping chapter of the VDM-SL
book by John Fitzgerald and Peter Gorm Larsen to introduce 
mappings and mapping operators concerns a system for tracking the 
movement of containers of hazardous material between phases of 
processing in a nuclear reprocessing plant. It is inspired by 
the formal model of a plant controller architecture developed 
by Manchester Informatics Ltd. in collaboration with British 
Nuclear Fuels (Engineering) Ltd. (BNFL) in 1995. More can be 
read about this in:

J.S. Fitzgerald and C.B. Jones, Proof in VDM: Case Studies, 
Chapter: Proof in the Validation of a Formal Model of a 
Tracking System for a Nuclear Plant, Springer-Verlag,
FACIT Series, 1998.

Language Version: vdm10
Entry point     : DEFAULT`Permission(tracker_inital,cid1,mk_token("Unpacking"))