Combining Model Learning and Model Checking to Analyze Java Libraries

In the current technological era, the correct functionality and quality of software systems are of prime concern and require practical approaches to improve their reliability. Besides classical testing, formal verification techniques can be employed to enhance the reliability of software systems. In this connection, we propose an approach that combines the strengths of two effective techniques, i.e., Model learning and Model checking for the formal analysis of Java libraries. To evaluate the performance of the proposed approach, we consider the implementation of “Java.util” package as a case study. First, we apply model learning to infer behavior models of Java package and then use model checking to verify that the obtained models satisfy basic properties (safety, functional, and liveness) specified in LTL/CTL languages. Our results of the formal analysis reveal that the learned models of Java package satisfy all the selected properties specified in temporal logic. Moreover, the proposed approach is generic and very promising to analyze any software library/package considered as a black-box.