Por Ian MacColl y David Carrington
La interfaz con el usuario es la frontera entre un sistema de computadora, compuesto de hardware y software y un usuario humano. El software de interfaz con el usuario es un componente significativo de los sistemas computacionales contemporáneos y las interfaces gráficas con el usuario son hoy en día casi universales.
La correctitud del software de una interfaz con el usuario es esencial para las aplicaciones críticas, tales como las que afectan la vida humana o la seguridad. La correctitud de la interfaz con el usuario es también importante para las aplicaciones que no son críticas porque la interfaz es el punto en donde el sistema es percibido por el usuario. El hacer pruebas es un método que es utilizado para determinar la correctitud del software, pero el hacer pruebas al software de una interfaz con el usuario es difícil.
Este artículo es concerniente al uso de métodos formales para incrementar la confianza en la correctitud del software de la interfaz con el usuario. Empezamos tomando en consideración nociones sobre la correctitud y maneras de obtener esta. Luego entonces introducimos métodos formales y delineamos la forma de cómo estos métodos pueden ser utilizados para incrementar la confianza en la correctitud del software. Finalmente, examinamos la aplicación de los métodos formales al desarrollo del software de la interfaz con el usuario e indicamos el potencial para el trabajo posterior sobre pruebas basadas en especificación de las interfaces con el usuario.
El Glosario Estándar de IEEE de la Terminología de Ingeniería de Software define correctitud en términos de estar libre de fallas, de satisfacer los requisitos especificados y satisfacer las necesidades y expectativas del usuario [20]. La correctitud del software es descrita más comúnmente como:
La correctitud es particularmente importante para el software en el cual la situación es crítica de alguna manera, por ejemplo cuando hay vidas humanas en riesgo. Nosotros esperaríamos que la correctitud de todos los aspectos de tal software, incluyendo la interfaz con el usuario, fuera con ahínco. Esto no es necesariamente el caso. Los accidentes Therac-25, ampliamente citados por muchos, los cuales resultaron en muertes y heridos, son atribuidos en parte a enriquecer la usabilidad de la interfaz con el usuario a expensas de la seguridad del sistema global [21].
La correctitud es importante para el software en general, así como particularmente importante para el software de la interfaz con el usuario. La interfaz con el usuario representa el aspecto del software que es directamente percibido por un usuario. Si la interfaz con el usuario es incorrecta, el software será percibido como incorrecto, aunque exista la correctitud de la funcionalidad subyacente.
La confianza de la correctitud de una interfaz con el usuario es usualmente lograda al hacer prototipos o por pruebas. Hacer prototipos puede ser usada para la validación y para verificar que la interfaz con el usuario cumpla con los requisitos de usabilidad. El hacer pruebas también puede ser utilizado para la validación (prueba de aceptación) y para evaluar la usabilidad. La prueba tradicional de software (unidad, integración y prueba del sistema) es el principal método para evaluar la correctitud del software de la interfaz con el usuario.
Aún cuando las pruebas del software de la interfaz con el usuario, particularmente software gráfico de la interfaz con el usuario, tiene elementos en común con otras pruebas de software, también presenta un número de retos:
En resumen, el software de interfaz con el usuario es complejo, altamente interactivo, sin modelar, concurrente, gráfico y tiene requisitos basados en el tiempo real del usuario. Las tecnologías emergentes de interfaz con el usuario tales como interacción multi-modal, multimedia, agentes inteligentes y computación y comunicaciones ubicuas, incrementarán los problemas de las pruebas.
Las herramientas industriales fuertes han sido desarrolladas para satisfacer estos desafíos. Estas herramientas proporcionan facilidades tales como captura/repetición para el desarrollo de pruebas, la evaluación de pruebas basadas en mapas de bits y en widget los scripts basados en lo textual y en el apunta-y-presiona. Aunque estos proporcionan el apoyo esencial para las pruebas del software de interfaz con el usuario, poco apoyo esta disponible para determinar que pruebas hay que realizar y después de haber decidido las pruebas, para decidir que salida es esperada de una prueba en particular.
Las definiciones al principio de esta sección indican que la correctitud es determinada con respecto a alguna expectativa o requerimiento especificado. La selección y evaluación de pruebas también pueden ser basadas en tal información. Los métodos formales proporcionan la forma para definir tal información y son el tema de la siguiente sección.
Los métodos formales (http://www.comlb.ox.ac.uk/archive/formal-methods.html) son "técnicas basadas matemáticamente para describir propiedades de un sistema" [33]. Estos típicamente incluyen una notación precisa para la construcción de modelos matemáticos de un sistema (de software). La notación es utilizada para especificar (en vez de diseñar o implementar) el sistema requerido y es concerniente a "lo que" es hecho por un sistema no tanto "como" es hecho. Dos características que definen a los métodos formales son abstracción y precisión.
Muchos métodos formales utilizan una notación con una apariencia matemática, pero esto no es un requisito. Por ejemplo, los lenguajes de programación con una base de sonido semántico pueden ser considerados como notaciones de especificación; ellas son notaciones precisas para construir modelos (ejecutables) de un sistema (aunque no sean particularmente abstractas). Las notaciones gráficas bien-definidas tales como las Redes de Petri Petri Nets (http://www.daimi.aau.dk/PetriNets) y las Cartas de Estado de Harel también son notaciones de especificación.
Los métodos formales pueden ser clasificados basados de acuerdo a su modelo, propiedad o comportamiento. Los métodos basados por su modelo o propiedad están relacionados con estructuras de datos de la modelación subyacente y sus operaciones, mientras que los métodos basados en comportamiento se enfocan en el comportamiento externamente observable.
Los métodos basados en modelo definen el comportamiento del sistema directamente construyendo un modelo utilizando estructuras matemáticas tales como conjuntos. Las notaciones basadas en modelo para sistemas secuenciales incluyen Z (http://www.comlab.ox.ac.uk/archive/z.html) y VDM (http://www.ifad.dk/vdm/vdm.html). Tales notaciones son apropiadas para especificar software que involucra estructuras de datos complejas y operaciones simples ya que los tipos de datos son explícitamente modelados.
Las notaciones basadas en propiedad tales como OBJ (http://www.comlab.ox.ac.uk/arhive/obj.html) y Larch (http://larchwww.lcs.mit.edu:8001/larch/) modelan tipos de datos implícitamente definiendo el comportamiento del sistema a través de un conjunto de propiedades. Los métodos basados en propiedad pueden ser clasificados adicionalmente como axiomáticos y algebraicos: los métodos axiomáticos están basados en la lógica predicados de primer orden y los métodos algebraicos utilizan axiomas ecuacionales.
Los métodos basados en comportamiento definen sistemas en términos de posibles secuencias de estados en vez de tipos de datos y son comúnmente utilizados para especificar los sistemas concurrentes y distribuidos. Las notaciones basadas en comportamiento incluyen las Redes de Petri , Cálculo de Sistemas de Comunicación (Calculus of Communicating Systems, CCS) (http://ei.cs.vt.edu/~cs5204/ccs.html), Proceso de Comunicación Secuencial (Communicating Sequential Processes CSP) (http://www.comlab.ox.ac.uk/archive/csp.html) y Cartas de Estado.
Los métodos formales pueden ser usados para incrementar la confianza en la correctitud del software por demostración, refinamiento y pruebas. La demostración, a veces llamada verificación formal, involucra una demostración rigurosa (usualmente involucrando la lógica deductiva) en la cual una implementación concuerda con su especificación. El refinamiento es el desarrollo de las implementaciones que son correctas por construcción; una especificación es rigurosamente transformada para derivar una implementación eficiente. El realizar pruebas involucra ejecutar una implementación con alguna entrada y comparar la salida resultante con la salida esperada de esa entrada. Las pruebas basadas en especificaciones utilizan una especificación (formal) para determinar entradas apropiadas y salidas esperadas.
Los métodos formales han sido apoyados por las aplicaciones en donde el costo del fallo del software es mayor que el presunto costo adicional del proceso del desarrollo formal, por ejemplo, para el software crítico de misión, seguridad y vida. La experiencia industrial indica, de cualquier modo, que los costos adicionales (por ejemplo, la capacitación del personal que usará los métodos formales) son más que compensados por otros ahorros.
Hall también publicó un artículo fundamental en 1990 en donde identificaba y desvanecía conceptos erróneos acerca de los métodos formales [11]. Su primer mito, "Los métodos formales pueden garantizar que el software es perfecto" resume una pretensión de que los métodos formales pueden eliminar las pruebas del software. Él contradice este mito señalando que, "Algunas cosas nunca pueden ser probadas y podemos equivocarnos en las demostraciones de las cosas que si podemos probar".
El punto de vista de Hall es reforzado por Bowen y Hinchey en su séptimo "mandamiento" para proyectos exitosos de métodos formales: "Probarás, prueba, prueba y prueba otra vez" [1]. Una especificación formal es una representación abstracta que puede ser transformada rigurosamente (refinada) a una implementación ejecutable. El proceso de transformación no puede ser completamente automatizado y el hacer pruebas puede indicar la posibilidad de un error (humano). El hacer pruebas también puede ser usado en el completo desarrollo formal para detectar fallas en el compilador o el sistema operativo usado para ejecutar el software.
El hacer pruebas del software es convencionalmente clasificado en pruebas del comportamiento y pruebas estructurales: las pruebas del comportamiento enfatizan las pruebas contra los requerimientos funcionales implementados por el software mientras que las pruebas estructurales enfatizan las pruebas basadas en la estructura interna del diseño e implementación del software.
La prueba estructural es principalmente usada para determinar si todas las partes del software han sido probadas; la prueba del comportamiento es usada para evaluar la correctitud del software. La definición precisa de comportamiento proporcionada por una especificación formal es particularmente útil para las pruebas del comportamiento como una base para derivar entradas de pruebas y como una manera para determinar la salida esperada de una entrad para una prueba en particular.
La aplicación de los métodos formales para hacer pruebas, también llamada hacer pruebas basadas en la especificación, es un tema de investigación activa. Gaudel, por ejemplo, resume pruebas de programa basadas en especificaciones algebraicas, describiendo métodos para seleccionar un subconjunto finito de un conjunto de pruebas exhaustivo [9]. Para las notaciones basadas en modelo, Horcher y Peleska muestran como las especificaciones Z pueden ser usadas para derivar los datos de entrada de una prueba y para evaluar automáticamente los resultados de una prueba [17]. La Prueba Template Framework y la metodología ClassBench son técnicas bajo investigación en la Universidad de Queensland, Australia. La Prueba Template Framework es una modelo abstracto y formal de realizar pruebas, usado para derivar una jerarquía de prueba de información, incluyendo entradas y salidas de prueba, de una especificación formal [2, 29, 30]. La Metodología ClassBench y la Prueba Template Framework proporcionan un enfoque a pruebas automatizadas de software orientado a objetos [16]. El proyecto de prueba basado en la especificación, financiado por el Consejo Australiano de Investigación y basado en el Centro de Investigación de Verificación de Software, involucra investigadores de la Universidad Rutgers, de Estados Unidos y la Universidad de Victoria, Canadá, y aspira a combinar la Prueba Template y ClassBench para crear métodos y herramientas para realizar pruebas de software orientado a objetos.
Esta sección ha introducido los métodos formales y ha delineado como ellos pueden ser usados para mejorar la confianza en la correctitud del software. La siguiente sección es un estudio de la aplicación de los métodos formales para el desarrollo del software para la interfaz con el usuario y también indica el potencial para trabajos adicionales sobre pruebas basadas en la especificación de interfaces con el usuario.
Los métodos formales han sido aplicados al desarrollo del software de interfaces con el usuario con dos finalidades: para abstracción de los detalles de los usuarios, de su software, y de su interacción, la base para razonar y para analizar y asegurar una implementación correcta del software requerido. La literatura de investigación aparece dominada por el trabajo concerniente con el análisis formal de HCI. Este artículo está relacionado con el uso de los métodos formales para lograr interfaces con el usuario correctas.
Took identifica dos paradigmas (o arquitecturas) para el software de interfaz con el usuario: el lingüístico y el basado en agentes [32]. El paradigma lingüístico esta basado en el trabajo de Foley y van Dam que distinguen los aspectos léxicos, sintácticos y semánticos de los lenguajes de comando interactivo. Las notaciones formales para el paradigma lingüístico son típicamente basadas sintácticamente y orientadas al comportamiento, como Backus-Naur Form (BNF) (http://phrantic.com/j_alan-/comp2.html#EBNF) [26] o diagramas de transición de estado [24] y no son bien apropiados para encargarse de la concurrencia o de la información semántica anexa.
Las arquitecturas basadas en agentes son un intento para resolver las limitaciones de las arquitecturas lingüísticas como una base para desarrollar las interfaces gráficas con el usuario. El paradigma basado en agentes encapsula datos, funcionalidad, entrada y salida dentro de un "agente" tal como un botón, una pantalla, o toda una interfaz con el usuario completa. Este encapsulamiento es consistente con el tipo de datos abstracto y con el desarrollo del software orientado a objetos.
La aplicación de los métodos formales a las arquitecturas basadas en agente es un tópico de investigación de actualidad. Así como el desarrollo del software orientado a objetos, las aproximaciones formales al desarrollo de las interfaces con el usuario basadas en agentes deberán dirigirse a ambos aspectos, el estático y el dinámico del sistema. Las notaciones basadas en modelo y basadas en propiedad son bien apropiadas para formalizar los aspectos estáticos, mientras que las notaciones basadas en comportamiento son preferibles para los aspectos dinámicos. Muchas aproximaciones formales basadas en agente utilizan notaciones múltiples de diferentes estilos, o extienden una notación existente para abarcar las capacidades de un estilo diferente.
Las notaciones basadas en comportamiento, tales como las Redes de Petri, son útiles para modelar comportamiento externo pero deben ser aumentadas para que incluyan los aspectos estáticos de las interfaces con el usuario. Palanque y Bastide, por ejemplo, utilizan el formalismo Objetos Cooperativos Interactivos (Interactive Cooperative Objects, ICO) para especificar, verificar e implementar las interfaces con el usuario [23]. El ICO proporciona un marco orientado a objetos para modelar los aspectos estáticos de un sistema y usa Redes de Petri para modelar los aspectos dinámicos.
Myers introduce un modelo para las "interfaces gráficas con el usuario altamente interactivas y manipuladas directamente" que encapsula la interacción dentro de objetos interactores [22]. El proyecto Esprit AMODEUS ha desarrollado dos métodos formales de interactores como encapsulamientos de un estado, eventos que manipulan el estado y un mecanismo para presentar el estado a los usuarios [4,3,13]. El primer modelo de interactor, desarrollado en CNUCE en Pisa, Italia, utiliza el proceso álgebra LOTOS (http://wwwtios.cs.utwente.nl/lotos), una notación basada en propiedad con capacidades de comportamiento. El modelo CNUCE es derivado de un trabajo sobre sistemas gráficos y dispositivos de entrada.
El segundo modelo interactor AMODEUS fue desarrollado en la Universidad de York, Reino Unido. El modelo de York utiliza notaciones basadas en modelo como Z y VMD, aumentadas por CSP para aspectos de comportamiento. El modelo de York es un desarrollo del trabajo de Sufrin y He [31] para extender Z para cubrir ambos, el aspecto estático así como el dinámico. El proyecto AMODEUS ha usado modelos de interactores para describir sistemas gráficos y para analizar sistemas interactivos. El trabajo actual incluye la integración de descripciones formales de usuarios y sistemas en un marco interactivo y una investigación de escalar el desarrollo formal de las implementaciones de la interfaz con el usuario.
Gran parte del trabajo que aplica métodos formales a la HCI enfatiza el análisis y el razonamiento en vez de la implementación. Un proyecto actual en la Universidad de Queensland [18, 19] esta interesado con las notaciones formales para las especificaciones (orientadas a objeto) del software de la interfaz con el usuario y el desarrollo de diseños utilizando transformaciones relativamente informales basadas en patrones de software [8]. Este proyecto esta usando Object-Z (http://www.cs.uq.edu.au/svrc/Object-Z) [27, 6], una extensión de Z orientada a objetos, para las especificaciones de interactores. El Object-Z enriquece las capacidades de Z basadas en modelo y con encapsulación construye e incluye operadores para expresar aspectos dinámicos tales como la concurrencia y la comunicación entre objetos.
Además del desarrollo basado formalmente, el hacer pruebas fue identificado arriba como una manera de mejorar la confianza en la correctitud del software. Hasta la fecha, el trabajo de Yip y Robson parece ser el único en utilizar los métodos formales para apoyar directamente el hacer pruebas para el software de interfaz con el usuario [34, 35]. Ellos utilizan tres notaciones para especificar el software de interfaz con el usuario: los diagramas de transición de estado para expresar las secuencias de interacción, una notación basada en modelo similar a Z para definir las transiciones del estado y una notación algebraica para el razonamiento. Las pruebas son derivadas de los diagramas de transición de estado y las especificaciones son usadas para determinar la salida esperada.
Una variación de pruebas basadas formalmente es el uso de restricciones en la implementación. Fisher y Frincke aumentan una notación algebraica especificada con axiomas desplegadas que conectan operaciones abstractas de aplicación con operaciones concretas de interfaz [7]. Los axiomas son usados para verificar la correctitud de la interfaz con respecto a la funcionalidad subyacente y son ejecutables para mantener la correspondencia de la interfaz y la funcionalidad a la hora de correrse. Las condiciones pre y pos booleanas son usadas para un propósito similar por Gieskins y Foley [10]. En efecto, las condiciones son una especificación y son usadas para controlar la visibilidad y habilitar para hacer prototipos y para generar documentación.
En este artículo hemos discutido la correctitud de la interfaz con el usuario y delineado las maneras de cómo se puede lograr a través de los métodos formales. Todavía existe considerable trabajo que realizar cuando se aplican los métodos formales para desarrollar el software de interfaz con el usuario.
Técnicas de desarrollo formal con escalamiento, tales como el refinamiento, para la producción de interfaces con el usuario de fuerza industrial es un tema de discusión abierto. Un aspecto particularmente interesante involucra la consideración de descomposición y refinamiento. Duke y Harrison [5] muestran que una especificación abstracta (Abs) puede ser refinada en especificaciones separadas de la interfaz con el usuario (Usr) y la funcionalidad de la aplicación (Fun) y que Fun es un refinamiento de Usr. (es decir, la interfaz con el usuario es una abstracción de la funcionalidad). Esto crea cuestionamientos para todo el proceso de desarrollo de software: el refinamiento de Abs a Usr a Fun enfatiza una aproximación al diseño orientado al usuario mientras que el refinamiento de Abs a Fun seguido por la derivación de Usr de Fun por abstracción enfatiza intereses de diseño orientado a sistemas. La deseabilidad del desarrollo interactivo y el uso de notaciones múltiples con nociones difiriendo del refinamiento añaden más complejidad a este tema.
La falta de trabajo sobre las pruebas basadas en especificación de interfaces con el usuario no es particularmente sorprendente dado la juventud relativa de estas dos áreas. Las pruebas basadas en especificación pueden proporcionar un uso intermedio de los métodos formales más allá de la simple especificación, sin los costos (y beneficios) de un proceso de desarrollo formal entero. Las técnicas existentes basadas en la especificación apuntan hacia particulares estilos de especificación así que la aplicación de estas técnicas debe considerar la integración de notaciones múltiples para cubrir ambos aspectos, el estático y el dinámico. La Prueba Marco Plantilla (Test Template Framework), por ejemplo, es bien apropiada para las pruebas basadas en la especificación de aspectos estáticos de especificaciones de la interfaz con el usuario basadas en modelo, pero es menos apropiada para poner a prueba los aspectos dinámicos. El proyecto de Prueba Basada en Especificación (Specification-Based Testing) está dirigido a probar los aspectos dinámicos de especificaciones formales orientados a objetos, pero es probable que se enfoque en la notación Object-Z. En nuestra propia investigación, estamos investigando opciones para extender la Prueba Marco Plantilla para acomodar notaciones múltiples o perspectivas para apoyar las pruebas basadas en especificación de las interfaces con el usuario.
Agradecemos a Anna Andrusiewicz y a Anthony MacDonald por haber leído un previo bosquejo de este artículo. Ian MacColl es apoyado por un Premio Australiano de Posgrado y por una beca de Posgrado del Laboratorio de Investigación Telstra.
Información de Autores
David Carrington ( http://www.cs.uq.edu.au/personal/davec; dave@cs.uq.edu.au) es un profesor en el Departamento de Ciencias Computacionales y un miembro académico del Centro de Investigación de Verificación de Software en la Universidad Queensland de Australia. Igual que su interés en la enseñanza de la ingeniería de software, su interés en investigación se enfoca al desarrollo de software para interfaces con el usuario. Esto incluye investigación en ambos, métodos y herramientas de soporte.