Verification of GSM-based artifact-centric systems through finite abstraction