Using Model Checking to Generate Test Cases for Critical Systems by Wei Ding