Catálogo de publicaciones

Compartir en
redes sociales

Navegación

Tipo

Acceso

Plataformas

Mostrar más

Temática

Mostrar más

Mostrando 10 de 166.819 registro(s)

tesis Acceso Abierto
Agregar a Mi catálogo

Verificación de software usando Alloy

Más información
Autores/as: Juan Pablo Galeotti ; Marcelo Fabián Frias

Disponibilidad
Institución detectada Año de publicación Navegá Descargá Solicitá
No requiere 2010 Biblioteca Digital (FCEN-UBA) (SNRD) acceso abierto

Cobertura temática: Lenguas y literatura  

La verificación acotada de software usando SAT consiste en la traducción del programa junto con las anotaciones provistas por el usuario a una fórmula proposicional. Luego de lo cual la fórmula es analizada en busca de violaciones a la especificación usando un SAT-solver. Si una violación es encontrada, una traza de ejecución exponiendo el error es exhibida al usuario. Alloy es un lenguaje formal relacional que nos permite automáticamente analizar especificiaciones buscando contraejemplos de aserciones con la ayuda de un SAT-solver off-the-shelf. Las contribuciones de la presente tesis son principalmente dos. Por un lado, se presenta una traducción desde software anotado en lenguaje JML al lenguaje Alloy. Para conseguir esto, se presenta: • DynAlloy, una extensión al lenguaje de especificación Alloy para describir propiedades dinámicas de los sistemas usando acciones. Extendemos la sintaxis de Alloy con una notación para escribir aserciones de correctitud parcial. La semántica de estas aserciones es una adaptación del precondición liberal más débil de Dijsktra. • DynJML, un lenguaje de especificación orientado a objetos que sirve de representación intermedia para facilitar la traducción de JML a DynAlloy. • TACO, un prototipo que implementa la traducción de JML a DynAlloy. En segundo lugar, introducimos una técnica novedosa, general y complementamente automatizable para analizar programas Java secuenciales anotados con JML usando SAT. Esta técnica es especialmente beneficiosa cuando el programa opera con estructuras de datos complejas. Para esto, se instrumenta el modelo Alloy con un predicado de ruptura de simetrías que nos permite el cómputo paralelo y automatizado de cotas ajustadas para los campos Java.
tesis Acceso Abierto
Agregar a Mi catálogo

Verificación tardía

Más información
Autores/as: Maria Luján Amarante

Disponibilidad
Institución detectada Año de publicación Navegá Descargá Solicitá
No requiere 2015 SEDICI: Repositorio Institucional de la UNLP (SNRD) acceso abierto

Cobertura temática: Economía y negocios  

La finalidad del tema elegido, pretende plasmar en estas páginas, una síntesis de las distintas particularidades que presenta el incidente de verificación tardía. En primer término se efectuará una descripción del proceso concursal desde sus orígenes, planteando las distintas alternativas que presenta y sus aspectos generales. Se desarrollarán con amplitud algunos conceptos de las situaciones particulares que hacen al incidente, planteando las posturas doctrinarias y de jurisprudencia más relevantes. En segundo término, se abordarán cuestiones específicas que hacen al rol del síndico y su incidencia frente al proceso. A continuación se desarrollará el tema de la imposición de costas, señalando el encuadre que la Ley de Concursos y Quiebras le da a la misma. En todos los temas analizados, se seguirá una metodología de desarrollo uniforme, presentando en primer lugar el marco legal, para efectuar luego su comparación con expresiones doctrinarias y jurisprudenciales.
tesis Acceso Abierto
Agregar a Mi catálogo

Verificación y alineación de procesos de negocio colaborativos

Más información
Autores/as: Jorge Roa ; Pablo Villareal ; Omar Chiotti

Disponibilidad
Institución detectada Año de publicación Navegá Descargá Solicitá
No requiere 2014 Repositorio Institucional Abierto de la Universidad Tecnológica Nacional (SNRD) acceso abierto

Cobertura temática: Economía y negocios  

Las colaboraciones inter-organizacionales permiten nuevas formas de gestión basadas en la cooperación. Los sistemas de información que brindan soporte a la gestión de estas acciones de colaboración requieren definir modelos y especificaciones de procesos de negocio colaborativos (PNCs) que representan el comportamiento explícito de la colaboración. En base a técnicas formales y a los conceptos del desarrollo dirigido por modelos, en esta tesis se proponen métodos y herramientas que permiten determinar el correcto comportamiento de los modelos de PNCs y, a partir de dichos modelos, generar especificaciones de PNCs cuyo comportamiento está alineado con el de los modelos. Se propone el lenguaje formal Redes de Interacción Global (GI-Nets) y un método de transformación para definir modelos formales de PNCs con GI-Nets a partir de modelos conceptuales de PNCs. Se definen dos métodos de verificación que permiten determinar si un modelo de PNC satisface un conjunto de propiedades que determinan su correcto comportamiento. El primer método, basado en GI-Nets, propone la propiedad de Solidez de Interacción Global de una GI-Net como principal criterio de verificación. Este método permite detectar el lugar específico donde existe un bloqueo en un modelo de PNC. El segundo método, basado en anti-patrones de comportamiento, provee un enfoque para especificar en forma sistemática los anti-patrones de cualquier lenguaje de PNCs. Este método detecta el lugar de un bloqueo y determina el conjunto de elementos que lo produce. Ambos métodos pueden ser utilizados con cualquier lenguaje de PNCs y dan soporte a la verificación de PNCs con constructores complejos. Se define un método formal de transformación de modelos que permite generar en forma automática una especificación de PNC cuyo comportamiento esté alineado con el definido en el modelo conceptual del PNC a partir del cual fue generada. Esto implica que el comportamiento de la especificación será correcto si el comportamiento del modelo del PNC es correcto, y viceversa. El método se utiliza para generar especificaciones de PNCs basadas en tecnologías de servicios Web a partir de modelos conceptuales de PNCs. Finalmente, se presentan las herramientas desarrolladas para la formalización, verificación y transformación de modelos y especificaciones de PNCs, y se utilizan las mismas para evaluar y validar los métodos propuestos en la tesis.
libros
Agregar a Mi catálogo

Verification Methodology Manual for SystemVerilog

Más información

ISBNs: 978-0-387-25538-5 (impreso) 978-0-387-25556-9 (en línea)

Disponibilidad
Institución detectada Año de publicación Navegá Descargá Solicitá
No detectada 2006 SpringerLink

Cobertura temática: Ingeniería eléctrica, electrónica e informática  

libros
Agregar a Mi catálogo

Verification of Object-Oriented Software. The KeY Approach: Foreword by K. Rustan M. Leino

Más información

ISBNs: 978-3-540-68977-5 (impreso) 978-3-540-69061-0 (en línea)

Disponibilidad
Institución detectada Año de publicación Navegá Descargá Solicitá
No detectada 2007 SpringerLink

Cobertura temática: Ciencias de la computación e información - Ingeniería eléctrica, electrónica e informática - Lenguas y literatura  

libros Acceso Abierto
Agregar a Mi catálogo

Verification-based software-fault detection

Más información

Disponibilidad
Institución detectada Año de publicación Navegá Descargá Solicitá
No requiere Directory of Open access Books acceso abierto
libros
Agregar a Mi catálogo

Verification, Model Checking, and Abstract Interpretation: 6th International Conference, VMCAI 2005, Paris, France, January 17-19, 2005, Proceedings

Más información

ISBNs: 978-3-540-24297-0 (impreso) 978-3-540-30579-8 (en línea)

Disponibilidad
Institución detectada Año de publicación Navegá Descargá Solicitá
No detectada 2005 SpringerLink

Cobertura temática: Ciencias de la computación e información  

libros
Agregar a Mi catálogo

Verification, Model Checking, and Abstract Interpretation: 7th International Conference, VMCAI 2006, Charleston, SC, USA, January 8-10, 2006, Proceedings

Más información

ISBNs: 978-3-540-31139-3 (impreso) 978-3-540-31622-0 (en línea)

Disponibilidad
Institución detectada Año de publicación Navegá Descargá Solicitá
No detectada 2006 SpringerLink

Cobertura temática: Ciencias de la computación e información - Ciencias físicas - Ingeniería eléctrica, electrónica e informática  

libros
Agregar a Mi catálogo

Verification, Model Checking, and Abstract Interpretation: 8th International Conference, VMCAI 2007, Nice, France, January 14-16, 2007. Proceedings

Más información

ISBNs: 978-3-540-69735-0 (impreso) 978-3-540-69738-1 (en línea)

Disponibilidad
Institución detectada Año de publicación Navegá Descargá Solicitá
No detectada 2007 SpringerLink

Cobertura temática: Ciencias de la computación e información - Medicina clínica  

libros
Agregar a Mi catálogo

Verification, Model Checking, and Abstract Interpretation: Third International Workshop, VMCAI 2002 Venice, Italy, January 21-22, 2002 Revised Papers

Más información

ISBNs: 978-3-540-43631-7 (impreso) 978-3-540-47813-3 (en línea)

Disponibilidad
Institución detectada Año de publicación Navegá Descargá Solicitá
No detectada 2006 SpringerLink

Cobertura temática: Ciencias de la computación e información - Ingeniería eléctrica, electrónica e informática - Medicina básica