Registro completo de metadatos
| Campo DC | Valor | Lengua/Idioma |
|---|---|---|
| dc.provenance | Repositorio Digital Universitario - Universidad Nacional de Córdoba | - |
| dc.contributor | D'Argenio, Pedro R. | - |
| dc.creator | Bordenabe, Nicolas Emilio | - |
| dc.date | 2011 | - |
| dc.date.accessioned | 2019-07-13T15:53:35Z | - |
| dc.date.available | 2019-07-13T15:53:35Z | - |
| dc.date.issued | 2011 | - |
| dc.identifier | Incluye referencias bibliográficas: p. 101-103. | - |
| dc.identifier | http://hdl.handle.net/11086/57 | - |
| dc.identifier.uri | http://rodna.bn.gov.ar/jspui/handle/bnmm/566707 | - |
| dc.description | Tesis (Lic. en Ciencias de la Computación)--Universidad Nacional de Córdoba. Facultad de Matemática, Astronomía y Física, 2011. | - |
| dc.description | Los sistemas tolerantes a fallas son aquellos que son capaces de seguir operando luego de la ocurrencia de una o más fallas. Una falla puede provocar cambios no deseados en el estado interno del sistema, y para que el sistema tolere la falla, deberá ser capaz de soportar estos cambios y continuar operando de la manera esperada. Los sistemas tolerantes a fallas son comunes en casos donde una falla no es aceptable, ya que la misma puede derivar grandes pérdidas, tanto económicas como de vidas humanas. Otra técnica para garantizar que un sistema funcione de la manera que corresponde es el model checking, una técnica de verificación automática que permite determinar se el modelo de un sistema cumple una propiedad determinada. En caso de que el sistema no satisfaga la propiedad, el model checker generalmente proporciona un contraejemplo de ayuda para determinar la fuente del error. En el presente trabajo se detallan los modelos e ideas usadas para la construcción de un model checker probabilista temporizado, pensado para la verificación de sistemas tolerantes a fallas. Se describirá el proceso de inyección de fallas en los modelos formales, la sintaxis del lenguaje de la herramienta, el proceso de traducción del mismo al lenguaje de PRISM (el model checker sobre el cual se provee la capa de abstracción), y la aplicación de la herramienta desarrollada a dos casos de estudio. | - |
| dc.description | Nicolás Emilio Bordenabe | - |
| dc.description | Manual de OFFBEAT -- Sintaxis formal de OFFBEAT -- Ejemplo de traducción de PRISM. | - |
| dc.format | application/pdf | - |
| dc.language | spa | - |
| dc.relation | Disponible en línea | - |
| dc.rights | info:eu-repo/semantics/openAccess | - |
| dc.source | reponame:Repositorio Digital Universitario (UNC) | - |
| dc.source | instname:Universidad Nacional de Córdoba | - |
| dc.source | instacron:UNC | - |
| dc.source.uri | http://hdl.handle.net/11086/57 | - |
| dc.subject | Software / Program Verification | - |
| dc.subject | Model checking | - |
| dc.subject | Sistema tolerante a fallas | - |
| dc.subject | Verificación formal | - |
| dc.title | OFFBEAT | - |
| dc.type | info:eu-repo/semantics/bachelorThesis | - |
| dc.type | info:eu-repo/semantics/acceptedVersion | - |
| dc.type | info:ar-repo/semantics/tesisDeGrado | - |
| Aparece en las colecciones: | Universidad Nacional de Córdoba. Repositorio Digital Universitario | |
Ficheros en este ítem:
No hay ficheros asociados a este ítem.