Especificación de modelos dinámicos y análisis automático de propiedades con herramientas basadas en Alloy
Tesis (Doctor en Ciencias de la Computación)--Universidad Nacional de Córdoba, Facultad de Matemática, Astronomía, Física y Computación, 2024.
| Autor principal: | |
|---|---|
| Otros Autores: | |
| Formato: | doctoralThesis |
| Lenguaje: | Español |
| Publicado: |
2024
|
| Materias: | |
| Acceso en línea: | http://hdl.handle.net/11086/553418 |
| Aporte de: |
| id |
I10-R141-11086-553418 |
|---|---|
| record_format |
dspace |
| spelling |
I10-R141-11086-5534182024-08-28T06:35:38Z Especificación de modelos dinámicos y análisis automático de propiedades con herramientas basadas en Alloy Cornejo, César Mauricio Regis, Germán Enrique Verificación de software Métodos formales Propiedades funcionales del software Lenguajes de especificación Propiedades dinámicas Análisis automatizado Alloy SAT solving Software verification Formal methods Software functional properties Specification languages Dynamic properties Automated analysis Chord protocol Tesis (Doctor en Ciencias de la Computación)--Universidad Nacional de Córdoba, Facultad de Matemática, Astronomía, Física y Computación, 2024. Fil: Cornejo, César Mauricio. Universidad Nacional de Córdoba. Facultad de Matemática, Astronomía, Física y Computación; Argentina. Los lenguajes de especificación son herramientas cada vez más utilizadas en el desarrollo de software, especialmente en etapas tempranas para analizar características del sistema en construcción. Alloy, un lenguaje de especificación formal, destaca por su sintaxis simple y su semántica relacional, junto con su capacidad de análisis automatizado eficiente. Aunque Alloy puede capturar propiedades estáticas y dinámicas, las segundas requieren construcciones complejas, lo que ha motivado el desarrollo de extensiones como DynAlloy y Electrum. Estas extensiones permiten capturar comportamientos dinámicos de manera más transparente. En particular, DynAlloy incluye un debugger que facilita la exploración de instancias de modelos, similar a un entorno de programación. Este trabajo compara ambas extensiones, analizando su expresividad, eficiencia, y aplicación en casos de estudio como el protocolo Chord. Specification languages are increasingly used tools in software development, especially in early stages to analyze system characteristics under construction. Alloy, a formal specification language, stands out for its simple syntax, relational semantics, and efficient automated analysis capabilities. Although Alloy can capture both static and dynamic properties, the latter require complex constructions, leading to the development of extensions like DynAlloy and Electrum. These extensions enable more transparent modeling of dynamic behaviors. In particular, DynAlloy includes a debugger that allows users to explore model instances in a way similar to a programming environment. This work compares both extensions, analyzing their expressiveness, efficiency, and application in case studies like the Chord protocol. Fil: Cornejo, César Mauricio. Universidad Nacional de Córdoba. Facultad de Matemática, Astronomía, Física y Computación; Argentina. 2024-08-27T14:47:51Z 2024-08-27T14:47:51Z 2024-07-29 doctoralThesis http://hdl.handle.net/11086/553418 spa Attribution-NonCommercial-ShareAlike 4.0 International http://creativecommons.org/licenses/by-nc-sa/4.0/ |
| institution |
Universidad Nacional de Córdoba |
| institution_str |
I-10 |
| repository_str |
R-141 |
| collection |
Repositorio Digital Universitario (UNC) |
| language |
Español |
| topic |
Verificación de software Métodos formales Propiedades funcionales del software Lenguajes de especificación Propiedades dinámicas Análisis automatizado Alloy SAT solving Software verification Formal methods Software functional properties Specification languages Dynamic properties Automated analysis Chord protocol |
| spellingShingle |
Verificación de software Métodos formales Propiedades funcionales del software Lenguajes de especificación Propiedades dinámicas Análisis automatizado Alloy SAT solving Software verification Formal methods Software functional properties Specification languages Dynamic properties Automated analysis Chord protocol Cornejo, César Mauricio Especificación de modelos dinámicos y análisis automático de propiedades con herramientas basadas en Alloy |
| topic_facet |
Verificación de software Métodos formales Propiedades funcionales del software Lenguajes de especificación Propiedades dinámicas Análisis automatizado Alloy SAT solving Software verification Formal methods Software functional properties Specification languages Dynamic properties Automated analysis Chord protocol |
| description |
Tesis (Doctor en Ciencias de la Computación)--Universidad Nacional de Córdoba, Facultad de Matemática, Astronomía, Física y Computación, 2024. |
| author2 |
Regis, Germán Enrique |
| author_facet |
Regis, Germán Enrique Cornejo, César Mauricio |
| format |
doctoralThesis |
| author |
Cornejo, César Mauricio |
| author_sort |
Cornejo, César Mauricio |
| title |
Especificación de modelos dinámicos y análisis automático de propiedades con herramientas basadas en Alloy |
| title_short |
Especificación de modelos dinámicos y análisis automático de propiedades con herramientas basadas en Alloy |
| title_full |
Especificación de modelos dinámicos y análisis automático de propiedades con herramientas basadas en Alloy |
| title_fullStr |
Especificación de modelos dinámicos y análisis automático de propiedades con herramientas basadas en Alloy |
| title_full_unstemmed |
Especificación de modelos dinámicos y análisis automático de propiedades con herramientas basadas en Alloy |
| title_sort |
especificación de modelos dinámicos y análisis automático de propiedades con herramientas basadas en alloy |
| publishDate |
2024 |
| url |
http://hdl.handle.net/11086/553418 |
| work_keys_str_mv |
AT cornejocesarmauricio especificaciondemodelosdinamicosyanalisisautomaticodepropiedadesconherramientasbasadasenalloy |
| _version_ |
1809206857904947200 |