CMC-UMC: a framework for the verification of abstract service-oriented properties

CMC and UMC are two prototypical instantiations of a common logical verification framework for the analysis of functional properties of service-oriented systems. The service-oriented SocL logic is used to describe the required system properties. Computational models of the system can be built either using the COWS specification language or designing the system as a collection of interacting UML state machines, and an on-the-fly model checker can be used to verify the satisfaction of the requirements and possibly to generate counterexamples or witnesses for them. An automotive case study is used to illustrate the overall framework.