  We consider the verification of current-state and K-step opacity for systems
modeled as interacting non-deterministic finite-state automata. We describe a
new methodology for compositional opacity verification that employs
abstraction, in the form of a notion called opaque observation equivalence, and
that leverages existing compositional nonblocking verification algorithms. The
compositional approach is based on a transformation of the system, where the
transformed system is nonblocking if and only if the original one is
current-state opaque. Furthermore, we prove that $K$-step opacity can also be
inferred if the transformed system is nonblocking. We provide experimental
results where current-state opacity is verified efficiently for a large
scaled-up system.
