Show simple item record

dc.contributorRubio Gimeno, Alberto
dc.contributor.authorLuengo Agulló, Cristina
dc.contributor.otherUniversitat Politècnica de Catalunya. Departament de Ciències de la Computació
dc.date.accessioned2015-10-01T13:46:02Z
dc.date.available2015-10-01T13:46:02Z
dc.date.issued2015-06-29
dc.identifier.urihttp://hdl.handle.net/2117/77255
dc.description.abstractNo es ningún secreto que tanto los sistemas software como hardware generalmente presentan errores. Los métodos de testeo y simulación pueden identificar muchos problemas importantes, pero para sistemas que tienen requerimientos de seguridad o que son económicamente críticos, es indispensable llevar a cabo una verificación exhaustiva. Tal análisis se puede realizar utilizando métodos de verificación formal. Un enfoque de la verificación formal es la verificación de modelos, que es un proceso totalmente automático basado en la construcción de modelos abstractos para representar sistemas. Poste- riormente, sobre estos modelos se comprueban propiedades deseadas del sistema, normalmente expresadas en alguna lógica temporal, como por ejemplo lógica linear temporal. Las propiedades expresadas con fórmulas de lógica linear temporal pueden describir el orden de los eventos en el tiempo sin describir el tiempo explícitamente. Por eso mismo, son útiles a la hora de verificar las posibles ejecuciones de un sistema. Este proyecto pretende implementar algoritmos de verificación de modelos que determinen si una fórmula de lógica linear temporal que exprese una propiedad de un cierto sistema es satisfecha por éste.
dc.description.abstractIt is no secret that computer software programs, computer hardware designs, and computer sys- tems in general exhibit errors. Testing and simulation methods can identify many significant problems, but for systems that have safety or economically critical requirements, exhaustive ver- ification is indispensable. Such exhaustive analysis can be performed with the use of formal verification methods. One approach to formal verification is model checking, which is a fully automated process based on the construction of abstract models to represent systems. These models are then checked against desired properties defining a specification, usually expressed in some temporal logic, such as linear temporal logic (LTL). Temporal properties can describe the ordering of events in time without introducing time explicitly, thereby being useful when verifying the possible executions of a system. This project aims to implement model checking algorithms that determine whether an LTL formula expressing a desired property is satisfied in a computing system.
dc.language.isoeng
dc.publisherUniversitat Politècnica de Catalunya
dc.subjectÀrees temàtiques de la UPC::Informàtica::Arquitectura de computadors
dc.subject.lcshAlgorithms
dc.subject.otherverificació formal
dc.subject.otherteoria d'autòmats
dc.subject.otherverificació de models
dc.subject.otherlògica lineal temporal
dc.subject.otherBüchi automata
dc.subject.otherformal verification
dc.subject.otherautomata theory
dc.subject.othermodel checking
dc.subject.otherlinear temporal logic
dc.subject.otherBüchi automata
dc.titleVerification of temporal properties of infinite state systems
dc.typeBachelor thesis
dc.subject.lemacAlgorismes
dc.identifier.slug109443
dc.rights.accessOpen Access
dc.date.updated2015-07-02T04:00:24Z
dc.audience.educationlevelGrau
dc.audience.mediatorFacultat d'Informàtica de Barcelona


Files in this item

Thumbnail

This item appears in the following Collection(s)

Show simple item record

All rights reserved. This work is protected by the corresponding intellectual and industrial property rights. Without prejudice to any existing legal exemptions, reproduction, distribution, public communication or transformation of this work are prohibited without permission of the copyright holder