Formalizing Alloy with a shallow embedding to Isabelle/HOL

Abstract

Formal methods are techniques developed with a mathematical basis in order to ensure a high level of quality on a software product. In this group of techniques there are some which favor the simplicity of use over the reliability of the results in order to reduce the resources that such approaches require. These so called "lightweight" formal methods emphasize partial specifications and rely on automatic analysis. Alloy is a declarative specification language designed to be "lightweight". It was designed along with a model checking tool named Alloy Analyzer which can automatically analyze specifications and search for counter examples in a limited small scope. However, sometimes model checking is not enough and unbounded verification is needed. In this work we defined a strategy to embed the logic of Alloy into the logic of the theorem prover Isabelle/HOL.We implemented a tool to automatically perform the shallow embedding, allowing the unbounded verification of Alloy specifications through the use of a theorem prover.

Métodos formais são técnicas desenvolvidas com uma base matemática cujo objetivo é garantir um elevado nível de qualidade num produto de software. Entre este conjunto de técnicas existem algumas que privilegiam a simplicidade de uso sobre a fiabilidade dos resultados, a fim de reduzir os recursos que estas abordagens exigem. Estes métodos formais conhecidos como "leves", enfatizam a especificação parcial e análise automática.

Alloy é uma linguagem de especificação declarativa criada para ser "leve". Ela foi criada juntamente com uma ferramenta de model checking designada por Alloy Analyzer que pode analisar automaticamente as especificações e procura contra exemplos num pequeno universo. Contudo, por vezes uma abordagem como model checking não é suficiente e a verificação total é necessária.

Neste trabalho definimos uma estratégia para incorporar a lógica do Alloy na lógica do theorem prover Isabelle/HOL e implementámos uma ferramenta para executar automaticamente essa tradução, permitindo a verificação de especificações em Alloy através do uso de um theorem prover.