In an interactive application, the term of visual feedback (rendering or application's visual response) is applied to any graphical form of communication directed from the application towards the user. In spite of visual feedback is predominant in current interactive applications and it is a usability factor that guide user task, the designer doesn't have any formal method to specify and to evaluate it. The present paper deals with the formal specification of visual feedback, and its relationship with the formal specification of the dialogue between interactive 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 some properties of an interactive application.

En una aplicación interactiva la retroalimentación visual es toda forma de comunicación en forma gráfica que va del sistema en dirección al usuario. A pesar que la retroalimentación visual predomina en los actuales aplicaciones interactivas y en particular es considerada como un factor de usabilidad que auxilia al usuario en su tarea, el diseñador no cuenta con un medio para especificarla y evaluarla explícitamente. Este articulo propone la especificación de la retroalimentación visual y su relación con la especificación formal de dialogo entre el sistema y el usuario. El trabajo primero clasifica la retroalimentación visual en diferentes categorías. Enseguida, se presentan los fundamentos del formalismo OCI el cual es propuesto para especificar la retroalimentación visual. Después, presentamos un caso de estudio ilustrando como diversas categorías de retroalimentación son tomadas en cuenta en el diseño de una aplicación interactiva. Finalmente mostramos como un análisis matemático puede ser desarrollado en el formalismo los OCI para verificar las propiedades de una aplicación interactiva.