Deriving a formal model of an interactive system from its UIL description in order to verify and to test its behaviour

  • Bruno d’Ausbourg
  • Guy Durrieu
  • Pierre Roche
Part of the Eurographics book series (EUROGRAPH)


This paper focuses on verifying and testing the interaction or dialogue between a user and an interactive system, especially in case of safety critical systems. In order to verify that the interface of a system behaves as intended by the user, we based our ongoing research on a compromise by allowing the use of informal (but practical) and formal methods. In fact, a formal description of the user’s interests and activities through the Interface seems very hard to produce by common designers. A more realistic attitude consists in deriving a formal model from the description of the intended interface as it was informally designed. Practically, a tool generates models in the language Lustre from a user’s UIL description and these models are used for verification or test purposes.


Internal State Formal Verification Output Flow Input Flow Verification Tool 
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, A. J. Dix. Integrating status and events phenomena in formal specifications of interactive systems. SIGSOFT’94, December 1994Google Scholar
  2. 2.
    G.D. Abowd. Formal Aspects of Human Computer Interaction. PhD thesis, University of Oxford Computer Laboratory: Programming Research Group, 1991.Google Scholar
  3. 3.
    G.D. Abowd, H.M. Wang and A.F. Monk. A formal technique for automated dialogue development, in Proceedings of the First Symposium on Designing Interactive Systems, DIS’95, Ann Arbor,MI, August 1995, ACM Press.Google Scholar
  4. 4.
    P. Bumbulis, P.S.C. Alencar, D.D. Cowan, C.J.P. Lucena, “Combining Formal Techniques and Prototyping in User Interfaces Construction and Verification” in Proceedings of the Eurographics Workshop DSVS-IS’ 95, Toulouse, France, June 95, Springer Computer Science, P. Palanque and R. Bastide edsGoogle Scholar
  5. 5.
    P. Caspi, D. Pilaud, N. Halbwachs and L. Plaice. Lustre: a declarative language for programming synchronous systems. In 14th ACM Symposium on Principles of Programming Languages, January 1987Google Scholar
  6. 6.
    J. Coutaz “Interfaces Homme-Machine: un regard critique” TSI vol 10(1), 1991Google Scholar
  7. 7.
    D. J. Duke, M.D. Harrison “Event model of a human system interaction” in Software Engineering Journal, January 95Google Scholar
  8. 8.
    G. Faconti, F. Paterno “An approach to the formal specification of the components of an interaction” in Eurographics 90Google Scholar
  9. 9.
    D.J. Duke and M.D. Harrison. Abstract Interaction Objects. Computer Graphics Forum, 12(3):25–26, 1993CrossRefGoogle Scholar
  10. 10.
    D.J. Duke and M.D. Harrison. Event Model of human system interaction. In Software Engineering Journal, Janauary 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 International workshop, Bari, 1994Google Scholar
  12. 12.
    J.R. Mc Graw. “The VAL Language: description and analysis”. TOPLAS, 4(1), January 1982Google Scholar
  13. 13.
    M. Green. “A survey of Three Dialogue Models”, ACM TRansactions on Graphics vol 5(3), July 1986Google Scholar
  14. 14.
    M.D. Harrison, D.J. Duke A review of Formalisms for describing Interactive Behaviour. In Proceedings of the ICSE’94 Worksho, R.N. Taylor and J. Coutaz, editors, Software Engineering and Human Computer Interaction; LNCS 896; May 1994Google Scholar
  15. 15.
    N. Halbwachs, P. Caspi, P. Raymond, D. Pilaud. The synchronous dataflow programming language LUSTRE. Proceedings of the IEEE 79(9):1305–1320, September 1991.CrossRefGoogle Scholar
  16. 16.
    N. Halbwachs, D. Pilaud, F. Ouabdesselam and A.C. Glory. Specifying, programming and verifying real time systems, using a synchronous declarative language. In Workshop on automatic verification methods for finite states systems, LNCS 407, Springer Verlag, June 1989.Google Scholar
  17. 17.
    D. Heller, P. Ferguson and D. Brennan. Motif Programming Manual, 2nd edition, February 1994.Google Scholar
  18. 18.
    G. Kahn. “The semantics of a simple language for parallel programming”. In IFIP 74, North Holland, 1974Google Scholar
  19. 19.
    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, pages 155–174. BCS HCI Specialist Group, Cambridge University Press, 1992.Google Scholar
  20. 20.
    F. Paterno, Definition of Properties of User Interfaces Using Action-Based Temporal Logic, in Proceedings of the 5’th International Conference on Software Engineering, pp 314–319, San Francisco, June 1993Google Scholar
  21. 21.
    F. Paterno and M. Mezzanotte, Formal Verification of undesired behaviours in the CERD case study, in Proceedings EHCI’95 Conference, Wyoming, August 1995.Google Scholar
  22. 22.
    D. Pilaud and N. Halbwachs. “From a synchronous declarative language to a temporal logic dealing with multiform time”. Formal Techniques in Real-Time amd Fault tolerant Systems, LNCS 331, Springer Verlag, September 1988Google Scholar
  23. 23.
    B. Sufrin and J. He, Specification, Analysis and refinement of interactive processes, in M. Harrison and H. Thimbley editors, Formal Methods in Human Computer Interaction, Cambridge University Press, 1990.Google Scholar

Copyright information

© Springer-Verlag/Wien 1996

Authors and Affiliations

  • Bruno d’Ausbourg
    • 1
  • Guy Durrieu
    • 1
  • Pierre Roche
    • 1
  1. 1.Centre d’Etudes et de Recherches de Toulouse - ONERAToulouseFrance

Personalised recommendations