Towards safety guarantees for service-oriented systems

In this paper I will address 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. I 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.