Introducción a TLA+ : especificación formal de marcapasos

Loading...
Thumbnail Image
Date
2018
Authors
Rodríguez Rodríguez, Lorenzo
Publisher
Universidad ORT Uruguay
DOI
ISSN
ISBN
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.
En
Thesis note
Proyecto (Carrera Universitaria). Universidad ORT Uruguay, Facultad de Ingeniería
Thesis degree name
Ingeniero en Sistemas
84 p. diagrs., tbls., grafs.
Notes
Incluye bibliografía y anexos
Incluye archivos complementarios.
Subject
VERIFICACIÓN FORMAL, TESTING, MARCAPASOS CARDÍACOS, PROYECTOS-ID, MÉTODOS FORMALES
Type
Trabajo final de carrera
Access the full text
Citation
Rodríguez Rodríguez, L. (2018). Introducción a TLA+: especificación formal de marcapasos (Proyecto). Universidad ORT Uruguay, Facultad de Ingeniería. Recuperado de https://rad.ort.edu.uy/handle/20.500.11968/3864
Rights license