Abstract
In this paper we present a method that aims to integrate the use of formal techniques in the design process of interactive applications, with particular attention to those applications where both usability and safety are main concerns. The method is supported by a set of tools. We will also discuss how the resulting environment can be helpful in reasoning about multi-user interactions using the task model of an interactive application. Examples are provided from a case study in the field of air traffic control.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
B. d’Ausbourg, C. Seguin, G. Durrieu, P. Roché, Helping the Automated Validation Process of User Interfaces Systems, Proceedings ICSE’98 pp.219–228.
G. Abowd, H. Wang, A. Monk, “A formal technique for automated dialogue development”, Proceedings DIS’95, ACM Press, pp.219–226.
G. Ballardin, C. Mancini, F. Paternò, Computer-Aided Analysis of Cooperative Applications, Proceedings Computer-Aided Design of User Interfaces, pp.257–270,, Kluwer, 1999.
G. Booch, J. Rumbaugh, I. Jacobson, Unified Modeling Language Reference Manual, Addison Wesley, 1999
R. De Nicola, A. Fantechi, S. Gnesi, and G. Ristori. An action-based framework for verifying logical and behavioural properties of concurrent systems, Computer Network and ISDN systems, 25, 1993, 761–778
J. Fernandez, H. Garavel, A. Kerbrat, R. Mateescu, L. Mounier, M. Sighireanu, CADP (CAESAR/ALDEBARAN Development Package): A Protocol Validation and Verification Toolbox, Proceedings of the 8th Conference on Computer-Aided Verification, LNCS 1102, Springer Verlag, pp. 437–440, 1996.
A. Hall, “Using Formal Methods to Develop an ATC Information System”, IEEE Software, pp.66–76, March 1996.
ISO (1988). Information Processing Systems — Open Systems Interconnection — LOTOS — A Formal Description Based on Temporal Ordering of Observational Behaviour. ISO/IS 8807. ISO Central Secretariat.
R. Mateescu and H. Garavel, XTL: A Meta-Language and Tool for Temporal Logic Model-Checking. Proceedings of the International Workshop on Software Tools for Technology. Transfer STTT’98 (Aalborg, Denmark), July 1998.
Myers, B., Rosson, M. B., “Survey on User Interface Programming”, Proceedings CHI’92, pp. 195–202, ACM Press, 1992.
P. Palanque, F. Paternò(eds.), Formal Methods in Human-Computer Interaction, Springer Verlag, 1997.
F. Paternò, Formal Reasoning about Dialogue Properties with Automatic Support, Interacting with Computers, August 1997, pp.173–196, Elsevier.
F. Paternò, Model-Based Design and Usability Evaluation of Interactive Applications, Springer Verlag, ISBN 1-85233-155-0, 1999.
F. Paternò, G. Faconti, On the Use of LOTOS to Describe Graphical Interaction, in Monk, Diaper & Harrison eds. People and Computers VII: Proceedings of the HCI’92 Conference, pp.155–173, Cambridge University Press.
A. Puerta, A Model-Based Interface Development Environment, IEEE Software, pp. 40–47, July/August 1997.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2001 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Paternò, F., Santoro, C. (2001). Integrating Model Checking and HCI Tools to Help Designers Verify User Interface Properties. In: Palanque, P., Paternò, F. (eds) Interactive Systems Design, Specification, and Verification. DSV-IS 2000. Lecture Notes in Computer Science, vol 1946. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-44675-3_9
Download citation
DOI: https://doi.org/10.1007/3-540-44675-3_9
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-41663-0
Online ISBN: 978-3-540-44675-0
eBook Packages: Springer Book Archive