Checking consistency between architectural models using SPIN