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

Simple item page
dc.contributor.advisorTasistro Souto, Álvaro Danieles
dc.contributor.tribunalYovine, Sergioes
dc.contributor.tribunalCornes Boquete, Cristina Roxanaes
dc.creatorRodríguez Rodríguez, Lorenzo
dc.date.accessioned2018-12-13T07:54:35Z
dc.date.available2018-12-13T07:54:35Z
dc.date.issued2018es
dc.descriptionIncluye bibliografía y anexoses
dc.descriptionIncluye archivos complementarios.es
dc.description.abstractEl 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.es
dc.format.extent84 p. diagrs., tbls., grafs.es
dc.identifier.citationRodrí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/3864es
dc.identifier.urihttp://hdl.handle.net/20.500.11968/3864
dc.languageEspañol.es
dc.publisherUniversidad ORT Uruguayes
dc.relation.otherhttps://bibliotecas.ort.edu.uy/bibid/88065es
dc.subjectVERIFICACIÓN FORMALes
dc.subjectTESTINGes
dc.subjectMARCAPASOS CARDÍACOSes
dc.subjectPROYECTOS-IDes
dc.subjectMÉTODOS FORMALESes
dc.titleIntroducción a TLA+es
dc.title.subtitleespecificación formal de marcapasoses
dc.typeTrabajo final de carreraes
ort.thesis.careerFI - Ingeniería en Sistemas - IDes
ort.thesis.degreegrantorFacultad de Ingenieríaes
ort.thesis.degreelevelCarrera Universitariaes
ort.thesis.degreenameIngeniero en Sistemases
ort.thesis.degreetypeProyectoes
ort.thesis.noteProyecto (Carrera Universitaria). Universidad ORT Uruguay, Facultad de Ingenieríaes
Files
Original bundle
Now showing 1 - 1 of 1
Thumbnail Image
Name:
Material completo.pdf
Size:
6.41 MB
Format:
Adobe Portable Document Format
Description:
description
Download
Collections
Trabajos finales de carrera de grado