Title
DynAlloy as a Formal Method for the Analysis of Java Programs
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.
Year
DOI
Venue
2006
10.1007/978-0-387-39388-9_24
INTERNATIONAL FEDERATION FOR INFORMATION PROCESSING
Keywords
Field
DocType
specification language,formal method
Scala,Programming language,Java annotation,Computer science,Java concurrency,Real time Java,Java API for XML-based RPC,Generics in Java,strictfp,Java Modeling Language
Conference
Volume
ISSN
Citations 
227
1571-5736
12
PageRank 
References 
Authors
0.75
13
2
Name
Order
Citations
PageRank
Juan P. Galeotti11669.64
Marcelo F. Frias229535.57