INVESTIGADORES
LOPEZ POMBO Carlos Gustavo
artículos
Título:
Alloy Analyzer+PVS in the Analysis and Verification of Alloy Specifications
Autor/es:
FRIAS, MARCELO FABIÁN; LOPEZ POMBO, CARLOS GUSTAVO; MOSCATO, MARIANO MIGUEL
Revista:
LECTURE NOTES IN COMPUTER SCIENCE
Editorial:
Springer Verlag
Referencias:
Lugar: Berlin, Germany; Año: 2007 vol. 4424 p. 587 - 601
ISSN:
0302-9743
Resumen:
This article contains two main contributions. On the theoretical side, it presents a novel complete proof calculus for Alloy. On the applied side we present Dynamite, a tool that combines the semiautomatic theorem prover PVS with the Alloy Analyzer. Dynamite allows one to prove an Alloy assertion from an Alloy specification using PVS, while using the Alloy Analyzer for the automated analysis of hypotheses introduced during the proof process. As a means to assess the usability of the tool, we present a complex case-study based on Zaves Alloy model of addressing for interoperating networks.
