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. Galeotti | 1 | 166 | 9.64 |
Marcelo F. Frias | 2 | 295 | 35.57 |