Verifying distributed real-time properties of embedded systems via graph transformations and model checking