My projekt goal is to extend PSYCO by a symbolic search algorithm to generate a termination criteria for the learning phase and to enable PSYCO to check properties on reactive systems.
The current JPF-PSYCO extension combines active automata learning and dynamic symbolic execution to generate interfaces of reactive components. Further in the accompanying theoretical work of Giannakopoulou et al. is shown, that this interfaces are k-full, in case they are safe, permissive, and tight for all method sequences of length up to k, k ϵ ℕ. The evaluation part of the current PSYCO implementation shows that the choice of k heavily influences the runtime behavior of PSYCO. Further it is argued, that it is possible to choose k to a relative small value after a manual analysis of the source code. During my project I will implement a symbolic search on the symbolic transition system produced by JDART to generate possible good choices for k in an automated manner. Apart of the choice of k the symbolic search output can also be used to prove invariants on the analyzed components, e.g., the absence of assertion violations.