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. © 2010 Springer-Verlag Berlin Heidelberg.
CITATION STYLE
Li, X., Hoover, H. J., & Rudnicki, P. (2010). API conformance verification for java programs. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 6447 LNCS, pp. 188–203). https://doi.org/10.1007/978-3-642-16901-4_14
Mendeley helps you to discover research relevant for your work.