Building reliable interactive systems has been identified as an important and difficult task from the late '60s. One approach to augment the reliability of interactive systems is to use formal models during system development. Formal methods have received attention for the design and analysis of human-computer interaction (HCI) for thirty years. The field of adaptive instructional systems (AIS) in general, and intelligent tutoring systems in particulars, have been mostly relying on empirical methods for training systems validation (the system supports learning), rather than formal methods for verification (the system meets its specifications). Empirical methods focus on the validity of pedagogical interventions at the individual task and problem sequence levels, using learning analytic methods such as Bayesian knowledge tracing, additive factors models, or machine learning models of human performance. The purpose of the paper is to explore some parallel and the applicability of HCI formal models to AIS. The paper: a) presents key concepts related to HCI formal models using semi-formal representations (workflow graphs), b) gives examples of formal properties to be verified, c) discuss briefly formal notations, and d) defines adaptive human-computer interaction. The last section of the paper discuss the similarity between HCI formal models and AIS standard modules, and identifies some area of applicability of HCI formal models to AIS design, recognizing the central value of AIS empirical methods at the foundation of AIS iterative design.
展开▼
