Resumen:
La verificación de modelos (en inglés model checking) es un método automático para verificar sistemas formales, escritos generalmente en algún tipo de lógica temporal. A lo largo de los años se fueron creando nuevas técnicas dentro de esta área para poder realizar la tarea más eficientemente. Una de ellas es conocida como Bounded Model Checking (BMC), que en general se trata de utilizar internamente procesos SAT para realizar la verificación deseada sobre un determinado modelo. FormaLex es una herramienta desarrollada para verificar coherencia de documentos normativos escritos en un lenguaje basado en lógica temporal. Internamente utiliza un model checker para poder constatar dicha coherencia. Sin embargo, existen casos en los que la información que estos brindan no es suficiente para determinar de manera certera que no existan incoherencias entre las normas legales analizadas. Este trabajo explora el uso del núcleo de insatisfacibilidad (unsat core) para refinar el análisis de FormaLex. Se documenta una modificación que se puede realizar dentro del model checker NuSMV (invocado por FormaLex para validar el modelo generado), en conjunto con el SAT solver Picosat, para que se pueda analizar el unsat core de la fórmula booleana generada al realizar BMC, contribuyendo así a detectar contradicciones entre fórmulas normativas.
Citación:
---------- APA ----------
Giménez, Francisco Andrés. (2017). Recuperación de fórmulas culpables mediante análisis de unsat core. (Tesis de Grado. Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales.). Recuperado de https://hdl.handle.net/20.500.12110/seminario_nCOM000644_Gimenez
---------- CHICAGO ----------
Giménez, Francisco Andrés. "Recuperación de fórmulas culpables mediante análisis de unsat core". Tesis de Grado, Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales, 2017.https://hdl.handle.net/20.500.12110/seminario_nCOM000644_Gimenez
Estadísticas:
Descargas mensuales
Total de descargas desde :
https://bibliotecadigital.exactas.uba.ar/download/seminario/seminario_nCOM000644_Gimenez.pdf
Distrubución geográfica
