Welcome!
To use the personalized features of this site, please log in or register.
If you have forgotten your username or password, we can help.
My Menu
Saved Items

Alloy Analyzer+PVS in the Analysis and Verification of Alloy Specifications

Marcelo F. Frias.Contact Information, Carlos G. Lopez PomboContact Information and Mariano M. MoscatoContact Information

(1)  Department of Computer Science, FCEyN, Universidad de Buenos Aires and CONICET,  
Abstract
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 semi-automatic 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 Zave’s Alloy model of addressing for interoperating networks.

Contact Information Marcelo F. Frias.
Email: mfrias@dc.uba.ar

Contact Information Carlos G. Lopez Pombo
Email: clpombo@dc.uba.ar

Contact Information Mariano M. Moscato
Email: mmoscato@dc.uba.ar
Fulltext Preview (Small, Large)
Image of the first page of the fulltext

References secured to subscribers.



Export this chapter
Export this chapter as RIS | Text
 
Remote Address: 38.107.191.114 • Server: mpweb17
HTTP User Agent: CCBot/1.0 (+http://www.commoncrawl.org/bot.html)