Abstract
In interactive systems, the term rendering applies to any form of communication directed from the application towards the users. The present paper deals with the specification of rendering, and its relationship with the formal specification of the dialogue between application and user. We first present a taxonomy of rendering according to its function in the application. We briefly recall the basics of the ICO formalism, which is used for the formal specification of the application. We then present a case study illustrating how various categories of rendering are taken into account in the ICO formalism. Lastly, we show how mathematical analysis can be performed on the ICO models to verify predictability properties of the interactive system.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Bastide, Rémi; Palanque, Philippe. Petri Net based design of user-driven interfaces using the Interactive Cooperative Objects formalism, in: Paternò, Fabio, Volume editor. Interactive systems: design, specification, and verification (DSV-IS’94). Springer-Verlag; 1994. pp. 383–400.
Bastide, Rémi; Palanque, Philippe. Implementation techniques for Petri net based specifications of human computer dialogues, in: Vanderdonkt, Jean, Editor. 2nd workshop on Computer Aided Design of User Interfaces, CADUI’96; Universite Notre-Dame de la Paix, Namur (Belgium). Presses Universitaires de Namur; 1996. pp. 285–302.
Bumbulis, Peter; Alencar, P.; Cowan, D.; Lucena, C. Combining formal techniques in user interface construction and verification, in: Palanque, Philippe; Bastide, Remi, Editors. 2nd Eurographics workshop on Design Specification and Verification of Interactive System (DSV-IS’95) Jun 7–9 1995; Toulouse, France. Springer-Verlag; 1995. pp. 174–192.
Campos, José C; Harrison, Michael. Formally verifying interactive systems: A review, in: Harrison, Michael; Torres, Juan C, Editors. 4th Eurographics workshop on Design, Specification and Verification of Interactive System (DSV-IS’97) Jun 4–6 1997; Granada, Spain. Springer-Verlag; 1997. pp. 109–124.
Carr, David. Interaction Object Graphs: an executable graphical notation for specifying user interfaces, in: Palanque, Philippe; Paternò, Fabio, Editors. Formal methods in Human-Computer Interaction. Springer-Verlag; 1997. pp. 141–155.
Coutaz, Joëlle; Nigay, Laurence; Salber, Daniel. Conceptual software architecture models for interactive system. ESPRIT BRA 7040 Amodeus-2; 1993 Mar. Report No.:WP11.
David, René; Alia, Hassane. Du Grafcet aux réseaux de Petri. Paris: Hermès; 1992.
Desel, Jörg; Esparza, Javier. Free choice Petri nets. Cambridge University Press; 1995. (Cambridge tracts on computer science; 40).
Dix, Alan J. Formal methods for interactive systems. Academic Press; 1991.
Author information
Authors and Affiliations
Consortia
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1998 Springer-Verlag Wien
About this paper
Cite this paper
Bastide, R., Palanque, P., Le, DH., Muñoz, J., LIS — FROGIS. (1998). Integrating rendering specifications into a formalism for the design of interactive systems. In: Markopoulos, P., Johnson, P. (eds) Design, Specification and Verification of Interactive Systems ’98. Eurographics. Springer, Vienna. https://doi.org/10.1007/978-3-7091-3693-5_12
Download citation
DOI: https://doi.org/10.1007/978-3-7091-3693-5_12
Publisher Name: Springer, Vienna
Print ISBN: 978-3-211-83212-7
Online ISBN: 978-3-7091-3693-5
eBook Packages: Springer Book Archive