Using Model Checking for the Automatic Validation of User Interfaces Systems

  • Bruno d’Ausbourg
Part of the Eurographics book series (EUROGRAPH)


This paper describes the prototype of a software environment devised for assisting the formal validation of user interfaces systems (UIS). It suggests an approach to include such formal operations in the design process. It explains why the UIS can be modelled properly by a dataflow system, how this model can be expressed by using equations of flows in the language Lustre and how techniques of model checking can be used to check properties on it and to generate tests. It describes then how these functions are integrated in a software environment prototype.


Model Check State Graph Safety Property Output Flow Input Flow 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    G.D. Abowd and A.J. Dix. Integrating status and event phenomena in formal specifications of interactive systems. SIGSOFT’94, ACM Press, pp. 44–52, 1994.Google Scholar
  2. 2.
    G.D. Abowd, H.M. Wang and A.F. Monk. A formal technique for automated dialogue development. In Proceddings of the First Symposium on Designing Interactive Systems, DIS’95,Ann Arbor, MI, ACM Press, August 1995.Google Scholar
  3. 3.
    B. d’Ausbourg, G. Durrieu and P. Roche. Deriving a formal model of an interactive system from its UIL description in order to verify and to test its behaviour. In Proceedings of DSVIS96, Namur, Belgium, June 1996.Google Scholar
  4. 4.
    B. d’Ausbourg, C. Seguin, G. Durrieu and P. Roche. Assisting the Automated Validation Process of User Interface Systems In Proceedings of the 20th International Conference on Software Engineering (ICSE’98), Kyoto, Japan, 1998.Google Scholar
  5. 5.
    P. Caspi, D. Pilaud, N. Halbwachs and J. Plaice. Lustre: a declarative language for programming synchronous systems, in 14th ACM Symposium on Principles of Programming Languages, January 1987.Google Scholar
  6. 6.
    D. Clement, T. Despeyroux, J. Incerpi, G. Kahn, B. Lang and V. Pascual. Centaur: the system. In Proceedings of SIGSOFT’88. Third Annual Symposium on Software Development Environments (SDE3), Boston, 1988.Google Scholar
  7. 7.
    A.J. Dix. Formal methods for interactive systems. Academic Press, 1991.Google Scholar
  8. 8.
    A.J. Dix and G.D. Abowd. Modelling status and event behaviour of interactive systems. In Software Engineering journal, November 1996.Google Scholar
  9. 9.
    D.J. Duke and M.D. Harrison. Abstract interaction objetcs. Computer Graphics Forum,1993, 12, n°3, pp. 25–26.CrossRefGoogle Scholar
  10. 10.
    D.J. Duke and M.D. Harrison. Event model of human system interaction. In Software Engineering journal, January 1995.Google Scholar
  11. 11.
    D.J. Duke, G. Faconti, M.D. Harrison and F. Paterno. Unifying views of interactors. In Proceedings of Advance Visual Interface’ 94 Workshop, Bari, 1994Google Scholar
  12. 12.
    M.D. Harrison and D.J. Duke. A review of formalisms for describing interactive behaviour. In Proceedings of the ICSE’94 Workshop, R.N Taylor and J. Coutaz, editors, Software Engineering and Human Computer Interaction, LNCS806, May 1994.Google Scholar
  13. 13.
    G. Faconti and F. Paterno. An approach to the formal specification of the components of an interaction. In Eurographics90, 1990.Google Scholar
  14. 14.
    N. Halbwachs, P. Caspi, P. Raymond and D. Pilaud. The synchronous dataflow programming language Lustre. In Proceedings of IEEE, number 9 in 79, pp. 1305–1320, September 1991.Google Scholar
  15. 15.
    N. Halbwachs, F. Lagnier and C. Ratel. Programming and verifying Real Time Systems by Means of the Synchronous DataFlow Programming Language Lustre. IEEE Transactions on Software Engineering, Special Issue on the Specification and Analysis of Real Time Systems, pp 795–793, Spetember 1992.Google Scholar
  16. 16.
    D. Heller, P. Ferguson and D. Brerinan. Motif Programming Manual. O’Reilly and Associates Inc, February 1994.Google Scholar
  17. 17.
    F. Paterno and G. Faconti. On the use of Lotos to describe graphical interaction. In A. Monk, D.Diaper, and M.D. Harrison, editors, People and Computers VII; HCI’92 Conference, BCS HCI Specialist Group, Cambridge University Press, 1992.Google Scholar
  18. 18.
    F. Paterno and M. Mezzanotte. Formal verification of undesired behaviours in the CERD case study. In Proceeedings EH CI’95 Conference, Wyoming, August 1995.Google Scholar
  19. 19.
    D. Pilaud and N. Halbwachs. From a synchronous delarative language to a temporal logic dealing with multiform time. In Symposium on Formal Techniques in Real Time and Fault Tolerant Systems, Springer Verlag, September 1988.Google Scholar

Copyright information

© Springer-Verlag Wien 1998

Authors and Affiliations

  • Bruno d’Ausbourg
    • 1
  1. 1.ONERA-CERTFrance

Personalised recommendations