U-Check: Model Checking and Parameter Synthesis Under Uncertainty