Abstraction, refinement and proof for probabilistic systems - McIver, Annabelle.; Morgan, Carroll , 1952- (Springer, 2005)