Introducción a TLA+

Abstract

El testeo de software es una de las fases cruciales del proceso de ingeniería de software y una de las más costosas tanto en recursos humanos como en tiempo dedicado a esta actividad. Se han desarrollado modelos y prácticas de desarrollo abocadas a la optimización de los resultados y la reducción de costos de esta fase dado que toda modalidad de desarrollo, independientemente de que modelo implemente, contiene esta etapa de testeo. Una de las técnicas utilizadas para la optimización del testeo son los métodos formales: lenguajes con una sintaxis que permite, basándose en distintas teorías y construcciones matemáticas, certificar de manera mecánica y automática que el software desarrollado satisface las propiedades deseadas. Dentro de la categoría de métodos formales existen múltiples lenguajes con variados propósitos que apuntan a ser utilizados en distintas etapas del proceso de desarrollo (especificación, implementación, verificación, etc.). El objetivo de este trabajo es realizar una presentación de TLA+ (Temporal Logic of Actions), que permite diseñar sistemas y modelarlos de forma tal de reducir la probabilidad de ocurrencia de errores en futuras etapas del desarrollo, y asegurar matemáticamente la satisfacción de distintas propiedades que el programa a diseñar deba cumplir. Se comenzará introduciendo la sintaxis de TLA+, presentando las estructuras que brinda el lenguaje para el modelado y la especificación de sistemas, para así continuar con la presentación de las herramientas que permiten, entre otras cosas, chequear de forma automática la especificación definida y realizar pruebas matemáticas del correcto cumplimiento de propiedades. Para finalizar, se especifican formalmente modos de marcapasos, ejemplificando así la utilidad de TLA+. Se concluye que la aceptación de este tipo de técnicas por parte de la industria implicaría múltiples beneficios para el proceso de construcción de software en su totalidad, tales como generar sistemas más rigurosos y certificados, permitir razonar de manera formal desde el estadio del diseño, reducir costos en las subsiguientes etapas del desarrollo, entre otros.