Towards Safety Guarantees for Service-Oriented Systems

In this paper the authors will addresses the problem of verifying that a service-oriented embedded system fulfills required safety guarantees. Services will be represented by collaborations among components with a varying number of participants. The services are equipped with rules for the instantiation and deletion of services, addition and removal of participants. Further a service's behavior could be modified at run-time. The authors will present techniques which are able to verify that such systems are safe with respect to a given specification. The sketched verification technique is able to cope with structural changes, run-time changes of rules and the run-time evolution of services.