| Sumario: | El análisis formal de especificaciones de software suele atacarse desde dosenfoques, usualmente llamados: liviano y pesado. En el lado liviano encontramoslenguajes fáciles de aprender y utilizar junto con herramientasautomáticas de análisis, pero de alcance parcial. El lado pesado nos ofrecelograr certeza absoluta, pero a costo de requerir usuarios altamente capacitados. Un buen representante de los métodos livianos es lenguaje de modelado Alloy y su analizador automático: el Alloy Analyzer. Su análisis consisteen transcribir un modelo Alloy a una fórmula proposicional que luego seprocesa utilizando SAT-solvers estándar. Esta transcripción requiere que el usuario establezca cotas en los tamañosde los dominios modelados en la especificación. El análisis, entonces, esparcial, ya que está limitado por esas cotas. Por ello, puede pensarse queno es seguro utilizar el Alloy Analyzer para trabajar en el desarrollo deaplicaciones críticas donde se necesitan resultados concluyentes. En esta tesis presentamos un cálculo basado en álgebras de Fork que permiterealizar demostraciones en cálculo de secuentes sobre especificaciones Alloy. También hemos desarrollado una herramienta (Dynamite) que loimplementa. Dynamite es una extensión del sistema de demostración semiatomático PVS, método pesado ampliamente utilizado por la comunidad. Así, Dynamite consigue complementar el análisis parcial que ofrece Alloy,además de potenciar el esfuerzo realizado durante una demostración usandoel Alloy Analyzer para detectar errores tempranamente, refinar secuentes yproponer términos para utilizar como testigos de propiedades cuantificadasexistencialmente.
|
|---|