Skip to main content
SpringerLink
Log in

Proving the Correctness of Formal User Interface Specifications

  • Conference paper
Design, Specification and Verification of Interactive Systems ’95

Part of the book series: Eurographics ((EUROGRAPH))

  • 47 Accesses

Abstract

Formal grammars, task action grammars and attribute grammars are widely accepted approaches for the specification of dialogues of interactive systems. In this paper we present a formal specification technique — based on attribute grammars — coupling dialogue specifications with application and layout specifications. For this specification formalism a proof principle and an analyzing technique is provided and applied to a user interface specification of an ISDN telephone. Properties can be shown between the interaction of a user and the behaviour of the system. The used specification technique allows e.g. to show that there are dialogues such that a special action can be performed, e.g. a menu-item can be selected and e.g. that the application has a special state after a distinguished action.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. B. Bauer: Attributed Term Induction — A Proof Principle for Attribute Grammars, technical report, Technische Universität München, TUM-I9403, February 1994

    Google Scholar 

  2. B. Bauer: A Unifying Concept for Algebraic Specifications and Attribute Grammars: Attributed Algebraic Specifications, technical report, to appear, 1995

    Google Scholar 

  3. B. Bauer, R. Hennicker: Proving the Correctness of Algebraic Implementations by the ISAR System, in: Proc. of the International Symposium on Design and Implementation of Symbolic Computation Systems 93, LNCS 722, Springer, Berlin, pp. 3–16, 1993

    Google Scholar 

  4. H. Balzert: Der JANUS-Dialogexperte: Vom Fachkonzept zur Dialogstruktur, Softwaretechnik, 93 (13), 1993

    Google Scholar 

  5. H. Balzert: Das JANUS-System, Informatik Forschung und Entwicklung, 1994

    Google Scholar 

  6. F. Bodart, A.-M. Hennebert, J.-M. Leheureux, I. Provot, J. M. Vanderdonckt: A Model-Based Approach to Presentation: A Continuum from Task Analysis to Prototype, Proc. of the Eurographics Workshop „Design, Specification and Verification of Interactive Systems, pp. 25–39, 1994

    Google Scholar 

  7. L. M. Chirica, D. F. Martin: An Algebraic Formulation of Knuthian Semantics, 17th Annual Symposium on Foundations of Computer Science, IEEE, Houston, Texas, 1976

    Google Scholar 

  8. L. M. Chirica, D. F. Martin: An Order-Algebraic Definition of Knuthian Semantics, Math. Systems Theory, 13, pp. 1–27, 1979

    Article  MATH  MathSciNet  Google Scholar 

  9. B. Courcelle, P. Deransart: Proofs of Partial Correctness for Attribute Grammars with Application to Recursive Procedures and Logic Programming, Information and Computation, 78, pp. 1–55, 1988

    Article  MATH  MathSciNet  Google Scholar 

  10. J. Coutaz: PAC, an implementation model for dialog design, Proc. of the INTERACT 87, Elsevier, pp. 431–436, 1987.

    Google Scholar 

  11. P. Deransart, M. Jourdan, B. Lorho: Attribute Grammars: Definitions, Systems and Bibliography, LNCS 323, Springer, Berlin, 1988

    Google Scholar 

  12. H. Ehrig, B. Mahr: Fundamentals of algebraic specifications 1, EATCS Monographs on Theoretical Computer Science, 6, Springer, Berlin, 1985

    Google Scholar 

  13. J. Eickel: Logical and Layout Structures of Documents, Computer Physics Communication, 61, pp. 201–208, 1990

    Article  MATH  Google Scholar 

  14. J. D. Foley, W. C. Kim, S. Kovacevic, K. Murray: UIDE - An Intelligent User Interface Design Environment, in: Intelligent User Interfaces, (eds.) J. W. Sullivan, S. W. Tyler, Addison Wesley, ACM Press, pp. 339–384, 1991

    Google Scholar 

  15. J. D. Foley, P. N. Sukaviriya, T. Griffith: A Second Generation User Interface Design Environment: The Model and the Runtime Architecture, Proc. ACM INTERCHI 93, Conference on Human Factors in Computing Systems, Model-Based User Interface Development System 93, pp. 375–382, 1993

    Google Scholar 

  16. U. Fraus: A Calculus for Conditional Inductive Theorem Proving, Proc. of the CTRS ‘92, Nancy, LNCS 656, Springer, 1993

    Google Scholar 

  17. U. Fraus: Mechanizing Inductive Theorem Proving in Conditional Theories, Ph.D thesis, Universität Passau, 1994

    Google Scholar 

  18. R. Hennicker: Context induction: a proof principle for behavioural abstractions and algebraic implementations. Formal Aspects of Computing, 3 (4), pp. 326–345, 1991.

    Article  MATH  Google Scholar 

  19. H. U. Hoppe: Task-Oriented Parsing - A Diagnostic Method to be Used by Adaptive Systems, Proceedings of ACM CHI’88 Conference on Human Factors in Computing Systems, pp. 241–247, 1988

    Google Scholar 

  20. Ch. Janssen, A. Weisbecker, J. Ziegler: Generating User Interfaces from Data Models and Dialogue Net Specifications, Proc. ACM INTERCHI 93, Conference on Human Factors in Computing Systems, Automated User Interface Generation, pp. 418–423, 1993

    Google Scholar 

  21. T. Katayama, Y. Hoshino: Verification of Attribute Grammars, 8th POPL, Williamsburg, VA, pp. 177–186, January 1981

    Google Scholar 

  22. G. Krönert, G. Lauber, H.-G. Mannes: Spezifikation, Prototyping und Implementierung von interaktiven Systemen und Verwendung von attributierten Grammatiken, Software-Entwicklung, pp. 225–238, 1989

    Google Scholar 

  23. A. Limpouch: Grammar-Based Formal Specification for the Object-Oriented User Interface Development, Proc. of the Eurographics Workshop „Design, Specification and Verification of Interactive Systems, pp. 317–334, 1994

    Google Scholar 

  24. U. Möncke, R. Wilhelm: Grammar Flow Analysis, in: Proceedings Attribute Grammars, Application and Systems, International Summer School SAGA, LNCS 545, Springer, Berlin, 1991

    Google Scholar 

  25. S. J. Payne: Task-Action-Grammars, Proc. INTERACT 84 Human-Computer Interaction, North-Holland, pp. 527–532, 1985

    Google Scholar 

  26. P. Reisner: Formal Grammar and Human Factors Design of an Interactive Graphics System, IEEE Transactions on Software Engineering, 7 (2), March 1981

    Article  Google Scholar 

  27. S. Schreiber: The BOSS System: Coupling Visual Programming with Model Based Interface Design, Proc. of the Eurographics Workshop „Design, Specification and Verification of Interactive Systems, pp. 41–60, 1994

    Google Scholar 

  28. S. Schreiber: Specification and Generation of User Interfaces with the BOSS System, Proc. East-West International Conference on Human-Computer Interaction EWHCI’94, 1994

    Google Scholar 

  29. M. J. Tauber: ETAG: Extended Task Action Grammars–A Language for the Description of the User’s Task Language, Proc. INTERACT 90 Human-Computer Interaction, North-Holland, pp. 163–168, 1990

    Google Scholar 

  30. J. A. Goguen, J. W. Thatcher, E. G. Wagner, J. B. Wright: Initial Algebra Semantics and Continuous Algebras, Journal of the Association of Computing Machinery, 24 (1), pp. 68–95, January 1977

    MATH  MathSciNet  Google Scholar 

  31. H. Qingyi: User Interface Specification with Attribute Grammars: A New Approach, Proc. 6th International Conference on Systems Research, Informatics and Cybernetics, Baden-Baden, 1992.

    Google Scholar 

  32. M. Wirsing: Algebraic Specifications, in: Handbook of Theoretical Computer Science, pp. 676–788, (ed.:) J. van Leeuwen, North Holland, 1990

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Institut für Informatik, Technische Universität München, Arcisstr. 21, D-80290, München, Germany

    Bernhard Bauer

Authors
  1. Bernhard Bauer
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. LIS/Université Toulouse I, Toulouse Cedex, France

    Philippe Palanque  & Rémi Bastide  & 

Rights and permissions

Reprints and permissions

Copyright information

© 1995 Springer-Verlag/Wien

About this paper

Cite this paper

Bauer, B. (1995). Proving the Correctness of Formal User Interface Specifications. In: Palanque, P., Bastide, R. (eds) Design, Specification and Verification of Interactive Systems ’95. Eurographics. Springer, Vienna. https://doi.org/10.1007/978-3-7091-9437-9_14

Download citation

  • DOI: https://doi.org/10.1007/978-3-7091-9437-9_14

  • Publisher Name: Springer, Vienna

  • Print ISBN: 978-3-211-82739-0

  • Online ISBN: 978-3-7091-9437-9

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation