Abstract
Software components, services, or modules are used via their application programming interface (API). For any sufficiently complex component, there are strict rules on the order and context in which particular methods of the API can be invoked. For example, a file must be opened before reading, and not read after closing. These constraints are called API conformance rules. Their violation at run-time creates errors, which are often subtle and difficult to diagnose. In general, API conformance rules cannot be statically checked if concurrency is involved. We present a verification framework, called Fex, that assists in Java API conformance verification. Fex operates as follows. The first step is to express the API conformance rules as executable specifications. Then, the program under investigation is instrumented such that all potential exceptions can be easily raised. Next, the program is sliced to retain only control flow and the relevant APIs. The executable API conformance rules and sliced program are then processed by the Java Path Finder model checker. Possible violations of the conformance rules are exhibited as exceptions during model checking. We have successfully applied our framework to the TSAFE reference air traffic control system and identified a subtle deadlock missed by previous verification efforts.
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
Java 2 platform api specification, http://download-llnw.oracle.com/javase/1.5.0/docs/api/index.html .
Betin-Can, A., Bultan, T., Lindvall, M., Lux, B., Topp, S.: Eliminating synchronization faults in air traffic control software via design for verification with concurrency controllers. Automated Software Engg. 14(2), 129–178 (2007)
Bierhoff, K.: Api protocol compliance in object-oriented software, PhD Thesis, Carnegie Mellon University, School of Computer Science (2009)
Bierhoff, K., Beckman, N.E., Aldrich, J.: Practical api protocol checking with access permissions. In: Drossopoulou, S. (ed.) ECOOP 2009 – Object-Oriented Programming. LNCS, vol. 5653, pp. 195–219. Springer, Heidelberg (2009)
DeLine, R., Fähndrich, M.: Typestates for objects. In: Odersky, M. (ed.) ECOOP 2004. LNCS, vol. 3086, pp. 465–490. Springer, Heidelberg (2004)
Dennis, G.: Tsafe: Building a trusted computing base for air traffic control software, Master’s Thesis, MIT (2003)
Fink, S., Yahav, E., Dor, N., Ramalingam, G., Geay, E.: Effective typestate verification in the presence of aliasing. In: ISSTA (2006)
Li, X.: Fex: A model checking framework for event sequences, Technical report TR08-14, University of Alberta (2008)
Li, X., James Hoover, H., Rudnicki, P.: Towards automatic exception safety verification. In: FM, pp. 396–411 (2006)
Lindvall, M., Rus, I., Shull, F., Zelkowitz, M.V., Donzelli, P., Memon, A.M., Basili, V.R., Costa, P., Tvedt, R.T., Hochstein, L., Asgari, S., Ackermann, C., Pech, D.: An evolutionary testbed for software technology evaluation. NASA Journal of Innovations in Systems and Software Engineering 1(1), 3–11 (2005)
Ramalingam, G., Warshavsky, A., Field, J., Goyal, D., Sagiv, M.: Deriving specialized program analyses for certifying component-client conformance. In: PLDI, pp. 83–94 (2002)
Reiss, S.P.: Specifying and checking component usage. In: AADEBUG, pp. 13–22 (2005)
Robillard, M.P., Murphy, G.C.: Static analysis to support the evolution of exception structure in object-oriented systems. ACM Trans. Softw. Eng. Methodol. 12(2), 191–221 (2003)
Strom, R.E., Yemini, S.: Typestate: A programming language concept for enhancing software reliability. IEEE Trans. Softw. Eng. 12(1), 157–171 (1986)
Visser, W., Havelund, K., Brat, G., Park, S., Lerda, F.: Model checking programs. Automated Software Engg. 10(2), 203–232 (2003)
Weiser, M.: Program slicing. IEEE Trans. Software Eng. 10(4), 352–357 (1984)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2010 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Li, X., Hoover, H.J., Rudnicki, P. (2010). API Conformance Verification for Java Programs. In: Dong, J.S., Zhu, H. (eds) Formal Methods and Software Engineering. ICFEM 2010. Lecture Notes in Computer Science, vol 6447. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-16901-4_14
Download citation
DOI: https://doi.org/10.1007/978-3-642-16901-4_14
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-16900-7
Online ISBN: 978-3-642-16901-4
eBook Packages: Computer ScienceComputer Science (R0)