Verification of Well-formedness in Message-Passing Asynchronous Systems modeled as Communicating Finite-State Machines