TAKOS stands for Toolbox for Analyzing the K-Opacity of Systems. TAKOS is the Java implementation of the theoretical results presented in [FM10] dedicated to the validation of several levels of opacity on systems..
- to check offline (i.e., model-check) the opacity of a secret on a system (Fig. a),
- to synthesize a runtime verification monitor in order to check online the opacity at system runtime (Fig. b),
- and to synthesize an enforcement monitor in order to ensure the opacity of a secret at system runtime (Fig. c).
One may consult the dedicated website for more information on TAKOS.