Specification-Based Verification and Validation of Web Services and Service-Oriented Operating Systems