Dynamite Alloy Analyzer+PVS in the Analysis and Verification of Alloy Specifications.pdfVIP

Dynamite: Alloy Analyzer+PVS in the Analysis and Verification of Alloy Specifications Marcelo F. Frias, Carlos G. Lopez Pombo Mariano M. Moscato Department of Computer Science Department of Computer Science FCEyN - Universidad de Buenos Aires FCEyN - Universidad de Buenos Aires and CONICET Argentina Argentina mmoscato@dc.uba.ar e-mail:{mfrias,clpombo}@dc.uba.ar Abstract to a close relational language based on binary relations (the calculus for omega closure fork algebras [4]). Since the re- This article contains two main contributions. On the the- sulting framework has a complete equational calculus, Al- oretical side, it presents a novel complete calculus for Alloy. loy was supplied with a complete equational calculus, too. On the applied side we present DYNAMITE, a tool that com- The translation process involved two main differences from bines the semi-automatic theorem prover PVS with the Alloy the source Alloy specification: Analyzer. DYNAMITE allows one to prove Alloy assertion • The resulting specification dealt only with binary rela- from Alloy specifications, while using the Alloy Analyzer for tions. Therefore, Alloy relations of greater arity had to the automated analysis of hypotheses introduced during the be encoded as binary relations. proof process. As a means to assess the usability of the tool, we present a complex case-study based on Zave’s model of