The state and situation calculus (SSC) that can be used for specifying distributed, reactive systems is shown to be quite convenient for reasoning about such specifications, not only for verification purposes but also when revising specifications found to be inappropriate. To this end, abductive reasoning techniques are established for SSC. This talk reports ongoing joint work with P. Gouveia.