Lessons Learnt on the Verification of Models Using Dynamite

MARIANO MOSCATO; CARLOS G. LOPEZ POMBO; MARCELO F. FRIAS

Río Cuarto, Argentina

Conferencia; Automatic Program Verification; 2009

Universidad Nacional de Rio Cuarto

Among other features the Dynamite Proving System (DPS) implements an assisted theorem prover for Alloy. The Alloy Analyzer has been used in the validation of realistic models outperforming similar tools available. It belongs to the class of the so called lightweight formal methods because of its low technical background required to be used. This last characteristic makes them very appealing for software engineers. In this paper we report our experience on using DPS in verifying an industrial size model for compositional bindings in network domains developed by Pamela Zave for AT&T. We also review the DPS foundations, architecture and some of its main features but we will focus on the experience using the tool in the verification of models.