FULL TITLE

Time modelling in interactive systems design

keywords

model checking, timing, human computer interaction

summary

In the case of modelling timing for design of interactive systems a feasibility study [2] has been completed (see general background) that is concerned with exploring the role of a timed model checker (uppaal [1]) in exploring properties of proposed designs. The aim is to help build designs to help users schedule activities dynamically. Timed model checking was used to understand the trade-offs associated with decisions and thereby to understand how the design could be constructed to assist users . The paintshop system was used as a relatively uncomplicated example also used in microworld simulations within DIRC.

The feasibility study raised important issues about the appropriate use of analysis techniques and problems associated with scaling these techniques. The analysis was used to answer questions such as: "Can all items be painted in t time units using one station?" and "Can all items be painted in t time units using both paint stations?". Traces that satisfied these questions as witnesses could be used to analyse best schedules and the means to support them. In practice the technique was expensive to apply and even small models generated an excessively large state space to explore. In addition further work is required to explore the human decision procedures that could be presumed by the model. This latter issue relates well to the work being carried out in the When To Act activity.

[1] Larsen, K.G., Pettersson, P. and Yi, W. (1997) Uppaal in a Nutshell. Int. Journal on Software Tools for Technology Transfer, 1(1-2): 134-152.

[2] Loer, K., Hildebrandt, M. & Harrison, M. (2004) Analysing dynamic function scheduling decisions.In Johnson and Palanque (editors) Human Error, Safety and Systems Development. Kluwer Academic. pp. 45-60

links

papers

Loer, K., Hildebrandt, M. & Harrison, M. (2004) Analysing dynamic function scheduling decisions.In Johnson and Palanque (editors) Human Error, Safety and Systems Development. Kluwer Academic. pp. 45-60

author

Michael Harrison (Newcastle)