Specifying and Verifying in Tuple Spaces