Abstract
JavaFAN uses a Maude rewriting logic specification of the JVM semantics as the basis of a software analysis tool with competitive performance. It supports formal analysis of concurrent JVM programs by means of symbolic simulation, breadth-first search, and LTL model checking. We discuss JavaFAN’s executable formal specification of the JVM, illustrate its formal analysis capabilities using several case studies, and compare its performance with similar Java analysis tools.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Brat, G., Havelund, K., Park, S., Visser, W.: Model checking programs. In: Automated Software Engineering 2000, pp. 3–12 (2000)
Broy, M., Wirsing, M., Pepper, P.: On the algebraic definition of programming languages. ACM Trans. on Prog. Lang. and Systems 9(1), 54–99 (1987)
Clavel, M., Durán, F., Eker, S., Lincoln, P., Mart´ı-Oliet, N., Meseguer, J., Talcott, C.: Maude 2.0 Manual (2003), http://maude.cs.uiuc.edu/manual
Clavel, M., Durán, F., Eker, S., Meseguer, J.: Building equational proving tools by reflection in rewriting logic. In: Proc. of the CafeOBJ Symposium (April 1998)
Cohen, R.M.: The defensive Java Virtual Machine specification. Technical report, Electronic Data Systems Corp (1997)
Corbett, J.C., Dwyer, M.B., Hatcliff, J., Laubach, S., P˘as˘areanu, C.S., Zheng, R., Zheng, H.: Bandera: extracting finite-state models from Java source code. In: International Conference on Software Engineering, pp. 439–448 (2000)
Demartini, C., Iosif, R., Sisto, R.: A deadlock detection tool for concurrent Java programs. Software - Practice and Experience 29(7), 577–603 (1999)
A. Farzan, F. Chen, J. Meseguer, and G. Roşu. JavaFAN. fsl.cs.uiuc.edu/javafan
Goguen, J., Malcolm, G.: Algebraic Semantics of Imperative Programs. MIT, Cambridge (1996)
Havelund, K., Lowry, M., Park, S., Pecheur, C., Penix, J., Visser, W., White, J.: Formal analysis of the remote agent before and after flight. In: The 5th NASA Langley Formal Methods Workshop (2000)
Havelund, K., Lowry, M., Penix, J.: Formal Analysis of a Space Craft Controller using SPIN. IEEE Transactions on Software Engineering 27(8), 749–765 (2001); Previous version appeared in Proceedings of the 4th SPIN workshop (1998)
Havelund, K., Pressburger, T.: Model checking Java programs using Java PathFinder. Software Tools for Technology Transfer 2(4), 366–381 (2000)
Holzmann, G.J.: The model checker SPIN. Software Eng 23(5), 279–295 (1997)
Jreversepro 1.4.1, http://jrevpro.sourceforge.net/
Kaufmann, M., Manolios, P., Moore, J.S.: Computer-Aided Reasoning: ACL2 Case Studies. Kluwer Academic Press, Dordrecht (2000)
Leavens, G.T., Leino, K.R.M., Poll, E., Ruby, C., Jacobs, B.: JML: notations and tools supporting detailed design in Java. Object Oriented Programming, Systems, and Applications, 105–106 (2000)
Meseguer, J.: Conditional Rewriting Logic as a Unified Model of Concurrency. Theoretical Computer Science, 73–155 (1992)
Moore, J.S.: http://www.cs.utexas.edu/users/xli/prob/p4/p4.html
Park, D.Y.W., Stern, U., Sakkebaek, J.U., Dill, D.L.: Java model checking. Automated Software Engineering, 253–256 (2000)
Plotkin, G.D.: A structural approach to operational semantics. Technical report, Computer Science Department, Aarhus University (1981)
Posegga, J., Vogt, H.: Java bytecode verification using model checking. In: Workshop Formal Underpinnings of Java OOPSLA (October 1998)
Roşu, G.: Programming Language Design - CS322 Course Notes
Stärk, R., Schmid, J., Börger, E.: Java and the Java Virtual Machine - Definition, Verification, Validation. Springer, Heidelberg (2001)
Stehr, M., Talcott, C.: Plan in Maude: Specifying an active network programming language. Rewriting Logic and its Applications, Electronic Notes in Theoretical Computer Science 71 (2002)
Thati, P., Sen, K., Mart´ı-Oliet, N.: An executable specification of asynchronous Pi-Calculus semantics and may testing in Maude 2.0. Rewriting Logic and its Applications, Electronic Notes in Theoretical Computer Science 71 (2002)
van den Berg, J., Jacobs, B.: The LOOP compiler for java and JML. In: Margaria, T., Yi, W. (eds.) TACAS 2001. LNCS, vol. 2031, p. 299. Springer, Heidelberg (2001)
Venners, B.: Inside The Java 2 Virtual Machine. McGraw-Hill, New York (1999)
Verdejo, A., Mart´ı-Oliet, N.: Executable structural operational semantics in Maude. Manuscript, Dto. Sistemas Informáticos y Programación, Universidad Complutense, Madrid (August 2003)
Wand, M.: First-order identities as a defining language. Acta Informatica 14, 337–357 (1980)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2004 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Farzan, A., Meseguer, J., Roşu, G. (2004). Formal JVM Code Analysis in JavaFAN. In: Rattray, C., Maharaj, S., Shankland, C. (eds) Algebraic Methodology and Software Technology. AMAST 2004. Lecture Notes in Computer Science, vol 3116. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-27815-3_14
Download citation
DOI: https://doi.org/10.1007/978-3-540-27815-3_14
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-22381-8
Online ISBN: 978-3-540-27815-3
eBook Packages: Springer Book Archive