Abstract
DynAHoy 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.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Ball, T, A Theory of Predicate-Complete Test Coverage and Generation. Technical Report MSR-TR-2004-28, Microsoft Research, Redmond, WA, April 20004.
Dijkstra E. W. and Scholten C. S., Predicate calculus and program semantics, Springer-Verlag, 1990.
Frias, M. F., Galeotti, J. P., Lopez Pombo, C. G., and Aguirre, N. M. DynAlloy: Upgrading Alloy with actions. In Proceedings of the 27th. International Conference on Software Engineering, G-C. Roman, Ed. Association for the Computer Machinery and IEEE Computer Society, ACM Press, St. Louis, Missouri, USA, 2005, 442–450.
Frias M.F., Lopez Pombo C.G., Baum G.A., Aguirre N.M. and Maibaum T.S.E., Reasoning About Static and Dynamic Properties in Alloy: A Purely Relational Approach, in ACM-Transactions on Software Engineering and Methodology (TOSEM), 14(4), 478–526, 2005.
Godefroid P., Klarlund N. and Sen K., DART: Directed Automated Random Testing, in Proceedings of the ACM SIGPLAN 2005 Conference on Programming Languages Design and Implementation (PLDI), 2005.
Goldberg, E. and Novikov, Y. BerkMin: A fast and robust sat-solver. In Proceedings of the conference on Design, automation and test in Europe, C. D. Kloos and J. da Franca, Eds. IEEE Computer Society, Paris, France, 142–149, 2000.
Gotlieb A., Denmat T. and Botella B., Constraint-Based Test Data Generation in the Presence of Stack-Directed Pointers, in Proceedings of ASE’05, Long Beach, CA, USA, ACM Press.
Harel D., Kozen D. and Tiuryn J., Dynamic Logic, MIT Press, October 2000.
Jackson, D. Alloy: a lightweight object modeling notation. ACM Transactions on Software Engineering and Methodology 11,2, 2002, 256–290.
Jackson D., Schechter I. and Shlyakhter I., Alcoa: the Alloy Constraint Analyzer, Proceedings of the International Conference on Software Engineering, Limerick, Ireland, June 2000.
Jackson D. and Vaziri, M., Finding Bugs with a Constraint Solver, in Proceedings of the International Symposium on Software Testing and Analysis (ISSTA), August 21–24, 2000, Portland, OR, USA. ACM, 2000, pp. 14–25.
JUnit: http://www.junit.org.
Khurshid S. and Marinov D., TestEra: Specification-Based Testing of Java Programs Using SAT., Automated Software Engineering 11(4): 403–434 (2004)
Gary T. Leavens, Albert L. Baker, and Clyde Ruby, Preliminary Design of JML: A Behavioral Interface Specification Language for Java. TR 98-06-rev27, Iowa State University, Department of Computer Science, April 2005.
Moskewicz, M. W., Madigan, C. F., Zhao, Y., Zhang, L., and Malik, S. Chaff: engineering an efficient SAT solver. In Proceedings of the 38th conference on Design automation, J. Rabaey, Ed. ACM Press, Las Vegas, Nevada, United States, 2001, 530–535.
Sen K., Marinov D. and Agha G., CUTE: A Concolic Unit Testing Engine for C, in Proceedings of the ACM SIGSOFT Conference on Foundations of Software Engineering, Lisbon, Portugal, 2005.
Visser W., Pasareanu C., Khurshid S., Test Input Generation with Java PathFinder, in Proceedings of the ACM/SIGSOFT International Symposium on Software Testing and Analysis, ISSTA 2004, Boston, Massachusetts, USA, July 11–14, 2004. ACM 2004, pp. 97–107.
Xie T., Marinov D., Schulte D. and Notkin D., Symtra: A Framework for Generating Object-Oriented Unit Tests Using Symbolic Execution, in Proceedings of TACAS 2005.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2006 International Federation for Information Processing
About this paper
Cite this paper
Galeotti, J.P., Frias, M.F. (2006). DynAlloy as a Formal Method for the Analysis of Java Programs. In: Sacha, K. (eds) Software Engineering Techniques: Design for Quality. IFIP International Federation for Information Processing, vol 227. Springer, Boston, MA. https://doi.org/10.1007/978-0-387-39388-9_24
Download citation
DOI: https://doi.org/10.1007/978-0-387-39388-9_24
Publisher Name: Springer, Boston, MA
Print ISBN: 978-0-387-39387-2
Online ISBN: 978-0-387-39388-9
eBook Packages: Computer ScienceComputer Science (R0)