DynAlloy as Formal Method For the Analysis of Java Programs

GALEOTTI, JUAN PABLO; FRIAS, MARCELO FABIAN

Springer IFIP Series

Springer

Lugar: Boston; Año: 2007 vol. 227 p. 249 - 260

1571-5736

Abstract. DynAlloy is an extension of the Alloy specification language that allows one to specify and analyze dynamic properties of models. The analysis is supported by the DynAlloy Analyzer tool. In this paper we present a method for translating sequential Java programs to DynAlloy. This allows one to use DynAlloy as a new formal method for the analysis of Java programs. As an application showing the utility of this formal method toward this task, we present JAT, a tool for automated generation of test data for sequential Java programs, implemented on top of the DynAlloy Analyzer.