Abstract
Java is a very successful programming language which is also becoming widespread in embedded systems, where software correctness is critical. Jlint is a simple but highly efficient static analyzer that checks a Java program for several common errors, such as null pointer exceptions, and overflow errors. It also includes checks for multi-threading problems, such as deadlocks and data races. The case study described here shows the effectiveness of Jlint in finding certain faults, including multi-threading problems. Analyzing the reasons for false positives in the multi-threading warnings gives an insight into design patterns commonly used in multi-threaded code. The results show that a few analysis techniques are sufficient to avoid almost all false positives. These techniques include investigating all possible callers and a few code idioms. Verifying the correct application of these patterns is still crucial, because their correct usage is not trivial.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Artho, C.: Finding Faults in Multi-Threaded Programs. Master’s thesis, ETH Zürich (2001)
Artho, C., Biere, A.: Applying Static Analysis to Large-Scale, Multi-threaded Java Programs. In: Grant, D. (ed.) Proceedings of the 13th ASWEC, pp. 68–75. IEEE CS Press, Los Alamitos (2001)
Artho, C., Havelund, K., Biere, A.: High-Level Data Races. In: VVEIS 2003 (April 2003)
Ball, T., Podelski, A., Rajamani, S.: Boolean and Cartesian Abstractions for Model Checking C Programs. In: Margaria, T., Yi, W. (eds.) TACAS 2001. LNCS, vol. 2031, p. 268. Springer, Heidelberg (2001)
Benowitz, E.G., Niessner, A.F.: Java for Flight Software. In: Space Mission Challenges for Information Technology (July 2003)
Bollella, G., Gosling, J., Brosgol, B., Dibble, P., Furr, S., Turnbull, M.: The Real-Time Specification for Java. Addison-Wesley, Reading (2000)
Brat, G., Giannakopoulou, D., Goldberg, A., Havelund, K., Lowry, M., Pasareanu, C., Venet, A., Visser, W.: Experimental Evaluation ofVerification andValidation Tools on Martian Rover Software. In: SEI Software Model Checking Workshop (2003) (Extended abstract)
Corbett, J., Dwyer, M.B., Hatcliff, J., Pasareanu, C.S., Robby, Laubach, S., Zheng, H.: Bandera: Extracting Finite-state Models from Java Source Code. In: Proc. 22nd International Conference on Software Engineering, Ireland, ACM Press, New York (2000)
Detlefs, D.L., Rustan, K., Leino, M., Nelson, G., Saxe, J.B.: Extended Static Checking. Technical Report 159, Compaq Systems Research Center, Palo Alto, California, USA (1998)
Godefroid, P.: Model Checking for Programming Languages using VeriSoft. In: Proc. 24th ACM Symposium on Principles of Programming Languages, France, pp. 174–186 (1997)
Gosling, J., Joy, B., Steele, G., Bracha, G.: The Java Virtual Language Specification, 2nd edn. Addison Wesley, Reading (2000)
Harrow, J.: Runtime Checking of Multithreaded Applications with Visual Threads. In: Havelund, K., Penix, J., Visser, W. (eds.) SPIN 2000. LNCS, vol. 1885, pp. 331–342. Springer, Heidelberg (2000)
Havelund, K.: Using Runtime Analysis to Guide Model Checking of Java Programs. In: Havelund, K., Penix, J., Visser, W. (eds.) SPIN 2000. LNCS, vol. 1885, pp. 245–264. Springer, Heidelberg (2000)
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: 5th NASA Langley Formal Methods Workshop, USA (June 2000)
Havelund, K., Pressburger, T.: Model Checking Java Programs using Java PathFinder. International Journal on Software Tools for Technology Transfer 2(4), 366–381 (2000)
Havelund, K., Roşu, G.: Monitoring Java Programs with Java Path Explore. In: Havelund, K., Roşu, G. (eds.) Runtime Verification (RV 2001). ENTCS, vol. 55, Elsevier Science, Amsterdam (2001)
Holzmann, G., Smith, M.: A Practical Method for Verifying Event-Driven Software. In: Proc. ICSE 1999, International Conference on Software Engineering, USA, IEEE/ACM (1999)
Lea, D.: Concurrent Programming in Java, 2nd edn. Addison Wesley, Reading (1999)
Lindholm, T., Yellin, A.: The Java Virtual Machine Specification, 2nd edn. Addison-Wesley, Reading (1999)
Sun Microsystems. Connected, limited device configuration. specification version 1.0a (May 2000), http://java.sun.com/j2me/docs/
Sun Microsystems. Java 2 documentation, http://java.sun.com/j2se/1.4/docs/
Savage, S., Burrows, M., Nelson, G., Sobalvarro, P., Anderson, T.: Eraser: A Dynamic Data Race Detector for Multithreaded Programs. ACM Transactions on Computer Systems 15(4), 391–411 (1997)
Stoller, S.D.: Model-Checking Multi-threaded Distributed Java Programs. In: Havelund, K., Penix, J., Visser, W. (eds.) SPIN 2000. LNCS, vol. 1885, pp. 224–244. Springer, Heidelberg (2000)
Visser, W., Havelund, K., Brat, G., Park, S.: Model Checking Programs. In: Proc. ASE 2000: The 15th IEEE International Conference onAutomated Software Engineering, IEEE CS Press, Los Alamitos (2000)
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
Artho, C., Havelund, K. (2004). Applying Jlint to Space Exploration Software. In: Steffen, B., Levi, G. (eds) Verification, Model Checking, and Abstract Interpretation. VMCAI 2004. Lecture Notes in Computer Science, vol 2937. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-24622-0_24
Download citation
DOI: https://doi.org/10.1007/978-3-540-24622-0_24
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-20803-7
Online ISBN: 978-3-540-24622-0
eBook Packages: Springer Book Archive