J.C. Campos, G. Doherty, and M.D. Harrison. Repository of models of interactive behaviour.

The UPPAAL pucketizer model referred to in G. Doherty, J. Campos and M.D. Harrison Resources for situated actions. T.C.N. Graham and P. Palanque (eds) Interactive Systems: Design, Specification and Verification. 15th International Workshop, DSVIS 2008. Springer Lecture Notes in Computer Science No. 3156. pp. 194-207. 2008.

Models referred to in: Jos´e Creissac Campos, Gavin Doherty, and Michael Harrison. Including User Behavior in Model Checking Analysis. Submitted for publication.

The PROMELA model of the photocopier

The first resourced PROMELA model of pucketizer

The PROMELA model of pucketizer with resources relating to position and schedule

The following model is one of a family of  MAL models

The ALARIS GP infusion pump (MAL)

Michael Harrison 10 November 2010