Towards an integrated proposal for Interactive Systems design based on TLIM and ICO

  • Philippe Palanque
  • Fabio Paterno
  • Rémi Bastide
  • Menica Mezzanotte
Conference paper
Part of the Eurographics book series (EUROGRAPH)


The importance of applying formal methods in the design and development process of Interactive Systems is increasingly recognised. However it is still an open issue the identification of systematic methods able to support designers and developers in specifying and demonstrating properties of user interfaces. TLIM and ICO are two formal methods which have been used for this purpose with interesting results. They address similar concepts but also have different features which allow us to consider useful their integrated use to obtain synergistic and complementary results. In this paper we show their application to some examples in order to discuss similarities and differences and we outline a proposal for their integrated use.


Interactive System Software Architecture Task Model Functional Core Temperature Translator 


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    J. Accot, S. Chatty & P. Palanque. A formal description of low level interaction and its application to multimodal interactive systems, in [10], Springer Verlag 1996.Google Scholar
  2. 2.
    P. Barnard, J. May, “Interactions with Advanced Graphical Interfaces and the Deployment of Latent Human Knowledge” in [8].Google Scholar
  3. 3.
    R. Bastide. Cooperative Objects: a formalism for the design of concurrent systems. PhD dissertation, University of Toulouse 1,1992 (in French).Google Scholar
  4. 4.
    R. Bastide & P. Palanque. A Petri net based environment for the design of event-driven interfaces. 16th international conference on Application and Theory of Petri nets, LNCS 935, Springer Verlag 1995.Google Scholar
  5. 5.
    R. Bastide & P. Palanque. Implementation techniques for Petri net based specifications of human computer dialogues. In proceedings of Computer Aided Design of User Interfaces (CADUI’96), Namur, June 1996, Presses Universitaires de Namur (Pub.).Google Scholar
  6. 6.
    S. K Card., T.P. Moran & A. Newell. The psychology of Human-Computer Interaction. Lawrence Erlbaum Associates, 1983.Google Scholar
  7. 7.
    R. DeNicola, A. Fantechi, S. Gnesi, G. Ristori, An Action Based Framework for Verifying Logical and Behavioural Properties of Concurrent Systems, Computer Networks & ISDN Systems, Vol.25, n° 7, February 1993, pp.761–778.CrossRefGoogle Scholar
  8. 8.
    Proceedings of the first Eurographics workshop on Design, Specification and Verification of Interactive Systems, F. Paternó Ed. Springer Verlag 1995, ISBN 3-540-59480-9.Google Scholar
  9. 9.
    Proceedings of the second Eurographics workshop on Design, Specification and Verification of Interactive Systems, P. Palanque & R. Bastide Eds. Springer Verlag 1995.Google Scholar
  10. 10.
    Proceedings of the third Eurographics workshop on Design, Specification and Verification of Interactive Systems, F. Bodart & J. Vanderdonckt Eds. Springer Verlag 1996.Google Scholar
  11. 11.
    P. Gray & C. Johnson, “Requirements for the Next Generation of User Interface Specification Languages”, Proceedings DSV-IS’95, Springer Verlag, pp.113–133.Google Scholar
  12. 12.
    R. Harston & P. Gray, “Temporal Aspects of Tasks in the User Action Notation”, Human Computer Interaction, Vol.7, pp.1–45.Google Scholar
  13. 13.
    IBM (1989) Systems Application Architecture, Common User Access. Advanced interface design guide. Package SDK Windows — June 1989.Google Scholar
  14. 14.
    ISO (1988) Information Processing Systems — Open Systems Interconnection — LOTOS — A Formal Description Technique Based on temporal Ordering of Observational Behaviour. ISO/IS 8807, ISO Central Secretariat.Google Scholar
  15. 15.
    D. Larrabeiti, J. Quemada, S. Pavón. From LOTOS to Petri nets through Iexpansion. Proceedings of the FORTE’96 conference Chapman & Hall, October 1996.Google Scholar
  16. 16.
    T. Moher, V. Dirda, R. Bastide & P. Palanque A bridging framework for modelling devices, users and interfaces. In [10], Springer Verlag 1996.Google Scholar
  17. 17.
    M. Mezzanotte & F. Paterno’, “Including Time in the Notion of Interactor”, Proceedings Workshop on Usability Aspect of Time, July’ 95, Glasgow and in SIGCHI bulletin vol 28, n°2, p. 57–61.Google Scholar
  18. 18.
    M. Mezzanotte & F. Paterno’, “Use of Task, User and Formal Models to Support Development of Multimedia Interactive Systems”, Proceedings of IFIP Working Conference Domain Knowledge for Interactive System Design, pp.213–226, May 1996, Chapman & Hall.Google Scholar
  19. 19.
    M. Mezzanotte & F. Paterno’, “Verification of Human-Computer Dialogues with an Infinite Number of States”, Proceedings Workshop on Formal Aspects of the Human Computer Interface, Sheffield, September’96, Springer Verlag.Google Scholar
  20. 20.
    P. Palanque. Modelling user-driven interfaces using the ICO formalism. PhD dissertation, University of Toulouse I, 1992 (in French).Google Scholar
  21. 21.
    P. Palanque, R. Bastide & L. Dourte (1993) Contextual Help for Free with the Formal Design of User Interfaces, HCI International’93, Elseiver, North Holland.Google Scholar
  22. 22.
    P. Palanque & R. Bastide. Petri net based design of user-driven interfaces using the interactive cooperative object formalism. In [8], p. 383–401.Google Scholar
  23. 23.
    P. Palanque & R. Bastide. Task Models — System Models: a Formal bridge over the Gap. In Critical Issues in User Interface System Engineering (Benyon & Palanque Eds.) Springer Verlag 1995.Google Scholar
  24. 24.
    P. Palanque & R. Bastide (1995) Verification of an Interactive Software by Analysis of its Formal Specification. Proceedings of Interact’95, Norway, Chapman et Hall.Google Scholar
  25. 25.
    P. Palanque & R. Bastide. Time modelling in Petri nets for the design of Interactive Systems. GIST workshop on Time in Interactive Systems. Glasgow, July 1995. SIGCHI bulletin vol 28 n°2, p. 43–46.CrossRefGoogle Scholar
  26. 26.
    P. Palanque & R. Bastide. Formal specification and verification of CSCW using the Interactive Cooperative Object formalism. People and Computer X. Proceedings of the HCF95 conference, Huddersfield, 1995, p. 213–232.Google Scholar
  27. 27.
    P. Palanque & R. Bastide. Performance evaluation as a tool for the formal design of interactive systems. IEEE Computational Engineering in Systems Applications (CESA’96) conference, Lille, July 1996, TERR Press.Google Scholar
  28. 28.
    P. Palanque, R. Bastide, C. Sibertin, L. Dourte (1993) Design of User-Driven Interfaces using Petri nets and Objects; CAISE’93. LNCS n° 685, Springer-Verlag.Google Scholar
  29. 29.
    J. Peterson. Petri nets and the modelling of systems. Prentice Hall, 1981.Google Scholar
  30. 30.
    F. Paterno’ & M. Mezzanotte, Analysing Matis through Interactors and ACTL, Amodeus II BRA Report, sm/wp36.Google Scholar
  31. 31.
    F. Paterno’ & M. Mezzanotte, “Formal Verification of Undesired Behaviours in the CERD Case Study”, Proceedings EHCI’95 IF1P Working Conference, Chapman&Hall Publisher, Wyoming, August 1995.Google Scholar
  32. 32.
    S. Pangoli & F. Paterno’, “Automatic Generation of Task-oriented Help”, Proceedings ACM Symposium on User Interfaces Software and Technology, pp. 181–187, ACM Press, Pittsburgh, November 1995.Google Scholar
  33. 33.
    F. Paterno’, S. Sciacchitano & J. Lowgren, “A User Interface Evaluation Mapping Physical User Actions to Task-driven Formal Specifications”, Proceedings DSV-IS’95, pp.35–53, Springer Verlag Publisher, Toulouse, June’95.Google Scholar
  34. 34.
    J. Rumbaugh, M. Blaha, W. Premerlani, F. Eddy, W. Lorensen. Object oriented modelling and design. Prentice Hall 1991.Google Scholar
  35. 35.
    C. Sibertin-blanc. A client server protocol for the composition of Petri nets. In proceedings of Application and Theory of Petri nets LNCS 691, USA, 1993.Google Scholar
  36. 36.
    A. Sutcliffe & P. Faraday, “Designing Presentations in Multimedia Interfaces”, Proceedings ACM CHI’94, pp.92–98.Google Scholar
  37. 37.
    S. Shlaer, S. Mellor. Object oriented systems analysis. Modelling the world in data. Yourdon Press, 1988.Google Scholar
  38. 38.
    R. Sisto & A. Valenzano, “Mapping Petri nets with Inhibitor Arcs onto Basic LOTOS Behaviour Expressions”, IEEE Transactions on Computers, Vol.44, N.12, December 1995, pp.1361–1370.CrossRefMATHGoogle Scholar

Copyright information

© Springer-Verlag/Wien 1996

Authors and Affiliations

  • Philippe Palanque
    • 1
    • 3
  • Fabio Paterno
    • 2
  • Rémi Bastide
    • 3
  • Menica Mezzanotte
    • 2
  1. 1.CENAToulouseFrance
  2. 2.CNUCE — CNRPisaItaly
  3. 3.LIS — IHMUniversité Toulouse IToulouseFrance

Personalised recommendations