Modular verification of correctness properties in an environment for concurrent systems specifications: the deadlock case