Upload resources

Upload your works to SEDICI to increase its visibility and improve its impact

 

Show simple item record

dc.date.accessioned 2018-04-24T12:34:12Z
dc.date.available 2018-04-24T12:34:12Z
dc.date.issued 2001
dc.identifier.uri http://hdl.handle.net/10915/66376
dc.description.abstract En el contexto de las aplicaciones industriales, existen distintos métodos formales propuestos que permiten el modelado de los elementos de este tipo de sistemas. La lógica P/PML (Product/Process Modeling Logic) es un método formal desarrollado para la especificación y construcción de sistemas industriales de tiempo real. Esta lógica es una extensión de la lógica dinámica de primer orden agregando (a) acciones atómicas arbitrarias en lugar de solo asignación, (b) variables sobre procesos que permiten especificar sistemas parcialmente, (c) un operador de paralelismo y (d) restricciones de tiempo sobre los procesos. En este trabajo se estudian los aspectos de verificación y derivación formal de procesos en la lógica P/PML. En la primer parte se define el formalismo P/PML, su sintaxis y semántica, y se dan algunos ejemplos de procesos en esta lógica. En la segunda parte de este trabajo se explora el concepto de verificación formal de procesos en P/PML, tratándose el aspecto de corrección parcial. Como resultado, se desarrolla un sistema formal de prueba que permite verificar la corrección parcial de procesos con respecto a especificaciones lógicas. En la tercer parte de este trabajo se explora el segundo concepto mencionado antes, el de derivación formal de procesos en la lógica P/PML, desarrollándose como resultado un calculo de refinamientos que permite derivar procesos a partir de especificaciones lógicas. Por ultimo, se presentan las conclusiones acerca de este trabajo y se citan algunas posibles extensiones a desarrollar en el futuro. es
dc.format.extent 89 p. es
dc.language es es
dc.title Verificación formal y refinamientos en P/PML es
dc.type Tesis es
sedici.creator.person Díaz, Javier Roberto es
sedici.subject.materias Ciencias Informáticas es
sedici.subject.keyword verificación formal es
sedici.subject.keyword lógica de programacion es
sedici.subject.keyword derivación de programas es
sedici.subject.keyword métodos formales es
sedici.description.fulltext true es
mods.originInfo.place Facultad de Informática es
sedici.subtype Tesis de grado es
sedici.rights.license Creative Commons Attribution-NonCommercial-NoDerivatives 4.0 International (CC BY-NC-ND 4.0)
sedici.rights.uri http://creativecommons.org/licenses/by-nc-nd/4.0/
sedici.contributor.director Baum, Gabriel Alfredo es
thesis.degree.name Licenciado en Informática es
thesis.degree.grantor Facultad de Informática es
sedici.date.exposure 2001-12-22
sedici.subject.acmcss98 Verification es
sedici.subject.acmcss98 Software es


Download Files

This item appears in the following Collection(s)

Creative Commons Attribution-NonCommercial-NoDerivatives 4.0 International (CC BY-NC-ND 4.0) Except where otherwise noted, this item's license is described as Creative Commons Attribution-NonCommercial-NoDerivatives 4.0 International (CC BY-NC-ND 4.0)