A Framework to Specify and Verify Computational Fields for Pervasive Computing Systems