Using Java PathFinder for Construction of Abstractions of Java Programs

• Main Author: Yuldashev, Nodir
• Other Authors: Poch, Tomáš
• Format: Dissertation
• Language: English
• Published: 2009
• Online Access: http://www.nusl.cz/ntk/nusl-275237

The growing complexity of software systems makes the verification of the systems very difficult. Techniques of formal verification and analysis are used to find bugs in the code, or to prove that the code satisfies some properties. A popular automated verification technique is model checking, which uses state space traversal. However, model checking is prone to state explosion and therefore does not scale to complex multi-threaded software systems. Common solution to this problem (state explosion) is to create an abstraction of the target system, and then verify only the abstraction. We have designed and implemented a tool for construction of abstraction of Java components in behavior protocols, which is based on the Java PathFinder model checker. Results of experiments on several non-trivial components show that the tool can be used in practice.