Take a look at the new version of this page: [ beta version ]. Tell us what you think.

ABSTRACT

This paper adresses the use of the model-checking technique to check the CARE properties of input multimodal interactions. Transition systems and temporal logic are used to specify a multimodal system and its properties. The properties of the multimodal interface are specified in the CTL temporal logic and checked by the SMV model checker.

REFERENCES

• 1: 1. Bellik Y. « Interfaces multimodales : concepts, modèles et architectures » thèse de doctorat d'université 1995.
• 2: Philip R. Cohen , Michael Johnston , David McGee , Sharon Oviatt , Jay Pittman , Ira Smith , Liang Chen , Josh Clow, QuickSet: multimodal interaction for distributed applications, Proceedings of the fifth ACM international conference on Multimedia, p.31-40, November 09-13, 1997, Seattle, Washington, United States [doi>10.1145/266180.266328]
• 3: 3. Coutaz J., Nigay L., Salber D., Blandford A., May J. and Young R.M. « Four easy pieces for assessing the usability of multimodal interaction: the CARE properties». In K. Nordby, P.H. Helmersen, D.J. Gilmore and S.A. Arnesen (eds) Human Computer Interaction: Interact '95. Chapman and Hall: London. pp. 115-120, 1995.
• 4: 4. Duke, D. et Harisson, M. D. « mapping User requirements to implementations ». In Software Engineering Journal, Vol 10(1), p54-75, 1997.
• 5: 5. MacColl et Carrington, D. "testing MATIS : a case study on specification-based testing of interactive systems", FAHCI (1998), pp. 57-69, ISBN 0-86339-7948.
• 6: 6. Nigay L. « Conception et modélisation logicielles des systèmes interactifs : application aux interfaces multimodales », PhD dissertation, Grenoble University, 1994, 315 pages.
• 7: 7. Nigay L., Coutaz J., « Espaces conceptuels pour l'interaction multimédia et multimodale », TSI, spéciale Multimédia et collecticiel, AFCET & HERMES Publ, Vol 15(9), 1996, p. 1195-1225.
• 8: 8. Fabio Paterno, Menica Mazzanotte. « Analysing Ma tis by Interactors and ACTL ». Amodeus Project Document : system Modelling/WP36, 1994.
• 9: 9. McMillan K. L., "The SMV system", Technical report, Carnegie Mellon University, 1992.
• 10: 10. P. Palanque, A. Schyn. « A model-based for Engineering multimodal interactive systems ». Proceeding of the ninth IFIP TC13 international Conference on Human-Computer Interaction (Interact'2003) sep 1-5, 2003. Zürich, Switzerland.

INDEX TERMS

Primary Classification:
  H. Information Systems
  H.5 INFORMATION INTERFACES AND PRESENTATION (I.7)
      H.5.2 User Interfaces (D.2.2, H.1.2, I.3.6)
          Subjects: Interaction styles (e.g., commands, menus, forms, direct manipulation)

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification

  F. Theory of Computation
  F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES
      F.4.1 Mathematical Logic

General Terms:
Design, Verification

Keywords:
formal methods, multimodal interaction