PSYCO for Reactive Systems

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.[1] 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.