Mostrar el registro sencillo del ítem

dc.contributor.advisorGallardo, María del Mar 
dc.contributor.authorSarabia Segura, Marina
dc.contributor.otherLenguajes y Ciencias de la Computaciónen_US
dc.date.accessioned2020-01-20T12:33:17Z
dc.date.available2020-01-20T12:33:17Z
dc.date.created2019-06
dc.date.issued2020-01-20
dc.identifier.urihttps://hdl.handle.net/10630/19196
dc.description.abstractLa construcción de software complejo puede verse asistida por los llamados métodos formales que permiten detectar errores de diseño e implementación, especialmente con respecto a las propiedades críticas del sistema. Los métodos formales son técnicas con una base matemática muy fuerte que les hace muy apropiados para el análisis y verificación del software. En este proyecto, hemos seleccionado un sistema complejo, como es la construcción de un sistema compuesto de varios ascensores que funcionan de manera coordinada. Este problema muestra muchos de los problemas típicos del desarrollo de software crítico. Por un lado, como cada ascensor funciona como un proceso autónomo que tiene que sincronizarse con el resto, la implementación del sistema puede contener los típicos errores de seguridad o viveza propios de los sistemas concurrentes. Por otro lado, la estructura del sistema de ascensores contiene varios componentes que se relacionan entre sí de múltiples formas. Finalmente, en el sistema de ascensores también hay propiedades de tiempo real que deberían satisfacerse para que su comportamiento sea aceptable. Cada tipo de propiedad requiere utilizar una técnica formal diferente. La mejor técnica formal para detectar errores propios de la interacción incorrecta entre procesos es el “Model Checking”[1,2,3]. En el model checking, los actores principales son los estados del sistema, y las transiciones que hacen que el sistema evolucione. Sin embargo, para analizar propiedades estructurales de los sistemas es mucho más fácil y eficiente usar lenguajes en los que la noción de clase y relación/asociación sea más explícita. En este proyecto, se ha utilizado el model checker SPIN, las herramientas Alloy, USE (para UML/OCL) y Uppaal para la descripción y análisis de las distintas propiedades deseables del sistema. Como resultado, se ha construido un sistema de ascensores que es correcto con respecto a las propiedades críticas del sistema.en_US
dc.language.isospaen_US
dc.rightsinfo:eu-repo/semantics/openAccessen_US
dc.rights.urihttp://creativecommons.org/licenses/by-nc-nd/4.0/*
dc.subjectAscensores - Programas de ordenadoren_US
dc.subjectMétodos formales (Informática)en_US
dc.subjectInformática - Trabajos Fin de Gradoen_US
dc.subjectGrado en Ingeniería del Software - Trabajos Fin de Gradoen_US
dc.subject.otherSistema de ascensores distribuidoen_US
dc.subject.otherVerificación de modelosen_US
dc.subject.otherModel checkingen_US
dc.subject.otherSPINen_US
dc.subject.otherUPPAALen_US
dc.subject.otherAlloy analyzeren_US
dc.subject.otherOCLen_US
dc.subject.otherLógica temporalen_US
dc.titleModelado, simulación y análisis de un sistema complejo de ascensoresen_US
dc.title.alternativeModeling, simulation, and analysis of a complex lift systemen_US
dc.typeinfo:eu-repo/semantics/bachelorThesisen_US
dc.centroE.T.S.I. Informáticaen_US
dc.rights.ccAttribution-NonCommercial-NoDerivatives 4.0 Internacional*


Ficheros en el ítem

Este ítem aparece en la(s) siguiente(s) colección(ones)

Mostrar el registro sencillo del ítem

Attribution-NonCommercial-NoDerivatives 4.0 Internacional
Excepto si se señala otra cosa, la licencia del ítem se describe como Attribution-NonCommercial-NoDerivatives 4.0 Internacional