Where academic tradition
meets the exciting future

You are here: TUCS > PUBLICATIONS > Publication Search > Reasoning About Interactive Sy...

Reasoning About Interactive Systems

Ralph Back, Anna Mikhajlova, Joakim von Wright, Reasoning About Interactive Systems. In: J. M. Wing, J. Woodcock, J. Davies (Eds.), Proceedings of the World Congress on Formal Methods (FM'99), Lecture Notes in Computer Science 1709, 1460–1476, Springer-Verlag, 1999.

Abstract:

The unifying ground for interactive programs and component-
based
systems is the interaction between a user and the system or between
a component and its environment. Modeling and reasoning about interactive
systems in a formal framework is critical for ensuring the systems'
reliability and correctness. A mathematical foundation based on the
idea of contracts permits this kind of reasoning. In this paper we
study an iterative choice contract statement which models an event
loop allowing the user to repeatedly choose from a number of actions
an alternative which is enabled and have it executed. We study
mathematical
properties of iterative choice and demonstrate its modeling capabilities
by specifying a component environment which describes all actions
the environment can take on a component, and an interactive dialog
box permitting the user to make selections in a dialog with the system.
We show how to prove correctness of the dialog box with respect to
given requirements, and develop its refinement allowing more complex
functionality and providing wider choice for the user.

Files:

Full publication in PDF-format

BibTeX entry:

@INPROCEEDINGS{pBaMiWr99a,
  title = {Reasoning About Interactive Systems},
  booktitle = {Proceedings of the World Congress on Formal Methods (FM'99)},
  author = {Back, Ralph and Mikhajlova, Anna and Wright, Joakim von},
  volume = {1709},
  series = {Lecture Notes in Computer Science},
  editor = {Wing, J. M. and Woodcock, J. and Davies, J.},
  publisher = {Springer-Verlag},
  pages = {1460–1476},
  year = {1999},
}

Belongs to TUCS Research Unit(s): Software Construction Laboratorium

Publication Forum rating of this publication: level 1

Edit publication