Show simple item record

dc.contributorTamura Morimitsu, Eugenio
dc.creatorArias Almeida, Jaime Eduardo
dc.date2012
dc.date.accessioned2015-11-20T15:24:26Z
dc.date.accessioned2016-08-02T14:38:27Z
dc.date.available2015-11-20T15:24:26Z
dc.date.available2016-08-02T14:38:27Z
dc.identifier.citationArias Almeida, J. E. (2012). Model checking for TCC calculus. Pontificia Universidad Javeriana, Cali.spa
dc.identifier.urihttp://hdl.handle.net/11522/7145
dc.descriptionLa Programación Concurrente por Restricciones (ccp) es un formalismo para modelar sistemas concurrentes en el cual agentes (procesos) interactúan con otros agregando (telling) y leyendo (asking) información representada como restricciones en un medio compartido (store). La Programación Concurrente Temporal por Restricciones (tcc), extiende el modelo ccp agregrándole constructores temporales para modelar agentes temporales y sistemas reactivos. La verificación formal cumple un papel muy importante en la detección de errores en sistemas concurrentes, ya que permite determinar si el modelo de un sistema satisface o no una propiedad. Model checking es una técnica de verificación formal que, dado el modelo de un sistema y una propiedad, comprueba sistemáticamente si el modelo satisface o no la fórmula. Este proyecto de grado investiga la técnica de model checking como un método formal para la verificación de programas tcc. La investigación se lleva a cabo mediante la definición de un algoritmo de model checking para el cálculo tcc. Para lograr esto, nosotros extendemos el algoritmo clásico de model checking para LTL. Primero definimos una estructura llamada tcc Structure la cual permite modelar el comportamiento de un sistema tcc, además describimos una lógica que permite razonar sobre programas tcc. Luego se presenta el grafo de model checking y las propiedades que debe cumplir para determinar que el modelo satisface la propiedad. Al final, se presenta un prototipo que implementa el algoritmo propuesto.spa
dc.description.abstractConcurrent Constraint Programming (ccp) is a formalism for concurrency in which agents (processes) interact with one another by adding (telling) and reading (asking) information represented as constraints in a shared medium (store). Temporal Concurrent Constraint Programming (tcc) extends ccp by adding temporal constructs for modeling timed and reactive systems. Formal verification plays an important role in detecting errors in concurrent systems since it allows to check whether or not a system satisfies a given property. Model checking is a formal verification technique that, given a finite-state model of a system and a property, it systematically checks whether the property is satisfied by the model. This project degree studies model checking as a formal method for the verification of tcc programs. The study is conducted by defining a model checking algorithm for tcc. To accomplish this, we extend the classical algorithm of model checking for LTL. We define a structure called tcc Structure which allows to model the behavior of a tcc system, and we then describe a specific logic which allows to reason about tcc programs. We also introduce the model checking graph and the properties that it must meet to determine that the model satisfies the property. Finally, we present a prototype which implements the proposed algorithm.spa
dc.formatapplication/pdfspa
dc.format.extent85 p.spa
dc.languagespaspa
dc.publisherPontificia Universidad Javerianaspa
dc.relationhttp://webview.javerianacali.edu.co/cgi-olib/?oid=562778spa
dc.rightsEl o los autores otorgan licencia de uso parcial de la obra a favor de la Pontificia Universidad Javeriana Seccional Cali, teniendo en cuenta que en cualquier caso, la finalidad perseguida siempre será facilitar, difundir y promover el aprendizaje, la enseñanza y la investigación. Con la licencia el o los autores autorizan a la Pontificia Universidad Javeriana Seccional Cali: la publicación en formato o soporte material, de acuerdo con las condiciones internas que la Universidad ha establecido para estos efectos. La edición o cualquier otra forma de reproducción, incluyendo la posibilidad de trasladarla al sistema o entorno digital. La inclusión en cualquier otro formato o soporte como multimedia, colecciones, recopilaciones o, en general, servir de base para cualquier otra obra derivada. La comunicación y difusión al público por cualquier procedimiento o medio (impreso o electrónico). La inclusión en bases de datos y en sitios web, sean éstos onerosos o gratuitos, existiendo con ellos previo convenio perfeccionado con la Pontificia Universidad Javeriana Cali para efectos de satisfacer los fines previstos. En estos eventos, tales sitios tendrán las mismas facultades que las aquí concedidas para la referida universidad, con las mismas limitaciones y condiciones. El o los autores continúan conservando los correspondientes derechos sin modificación o restricción alguna, puesto que de acuerdo con la legislación colombiana aplicable, el acuerdo jurídico con la Pontificia Universidad Javeriana Cali, en ningún caso conlleva la enajenación del derecho de autor y de sus conexos. EL AUTOR, expresa que el artículo, folleto o libro objeto de la presente autorización es original y la elaboró sin quebrantar ni suplantar los derechos de autor de terceros, y de tal forma, el recurso electrónico aquí presentado es de su exclusiva autoría y tiene la titularidad sobre éste. PARÁGRAFO: en caso de queja o acción por parte de un tercero referente a los derechos de autor sobre el recurso electrónico en cuestión, EL AUTOR, asumirá la responsabilidad total, y saldrá en defensa de los derechos aquí autorizados; para todos los efectos, la Pontificia Universidad Javeriana Cali actúa como un tercero de buena fe.spa
dc.rights.urihttp://creativecommons.org/licenses/by-nc-nd/2.5/co/*
dc.subjectFacultad de Ingenieríaspa
dc.subjectCarrera de Sistemas y Computaciónspa
dc.subjectModel checkingspa
dc.subjectprogramación concurrente temporal por restriccionesspa
dc.subjectverifi- cación formal automáticaspa
dc.titleModel checking for TCC calculusspa
dc.typeinfo:eu-repo/semantics/bachelorThesisspa
dc.audiencePontificia Universidad Javeriana communityspa
dc.contributor.roleConsultor de tesisspa
dc.coverageCali; Lat: 03 24 00 N degrees minutes; Lat: 3.4000 decimal degrees; Long: 076 30 00 W degrees minutes; Long: -76.5000 decimal degreesspa
dc.creator.degreeIngeniero de Sistemas y Computación e Ingeniero Electrónicospa
dc.publisher.facultyFacultad de Ingenieriaspa
dc.publisher.programCarrera de Ingeniería de Sistemas y Computaciónspa
dc.pubplace.cityCalispa
dc.rights.accesoAcceso cerradospa
dc.rights.accessRightsinfo:eu-repo/semantics/closedAccessspa
dc.rights.ccAtribución-NoComercial-SinDerivadas 2.5 Colombia*
dc.source.repositoryreponame:Acervo Institucional: Repositorio Institucional PUJspa
dc.source.institutioninstname:Pontificia Universidad Javeriana Cali.spa
dc.type.hasversioninfo:eu-repo/semantics/acceptedVersionspa
dc.type.spaTrabajo de Gradospa


Files in this item

Thumbnail
Thumbnail

This item appears in the following Collection(s)

Show simple item record

Atribución-NoComercial-SinDerivadas 2.5 Colombia
Except where otherwise noted, this item's license is described as Atribución-NoComercial-SinDerivadas 2.5 Colombia