La tecnología móvil ha surgido de la necesidad de las personas de llevar consigo un medio de comunicación con opciones de entretenimiento, una biblioteca y acceso a Internet. Actualmente, se ha masificado el uso de dispositivos móviles inteligentes (smart) que se utilizan como algo más que un mero medio de comunicación. Desde un dispositivo móvil smart se puede, por ejemplo, tomar fotografías, gestionar cuentas bancarias, localizar restaurantes y comercios cercanos a la ubicación geográfica del usuario, registrar las actividades físicas diarias, e incluso mostrar indicadores biométricos y de salud.
El escenario de verificación de las Apps es muy distinto y más exigente que el de las aplicaciones que se ejecutan en PC. En primer lugar, el funcionamiento de las Apps puede variar entre dispositivos, esto significa que las Apps se deben analizar físicamente en varios modelos de dispositivos. En segundo lugar, cualquier programa de análisis puede corromper el funcionamiento normal de un dispositivo, por lo que una buena alternativa para analizar las Apps sin comprometer los resultados es utilizar dispositivos externos. Finalmente, las secuencias de acciones que sigue el usuario utilizando las Apps pueden dar lugar a fallos que no son identificados con facilidad en tiempo de desarrollo, por este motivo el comportamiento del usuario debe formar parte del análisis de las Apps.
En este trabajo se presenta una propuesta integrada para analizar propiedades extra-funcionales en tiempo de ejecución de aplicaciones móviles que utiliza de forma conjunta los métodos formales: Model Checking , Model Based Testing y Runtime Verification. La propuesta inicia con un modelo formal de todos los posibles comportamientos ejecutados por un usuario sobre una o varias Apps, de manera que se representan todas las acciones potenciales del usuario. Entonces, se explora exhaustivamente el modelo, utilizando la técnica de Model Checking, para generar un conjunto de casos de prueba.
Buscar en Dimension