Automatic Component Protocol Generation and Verification of Components

In several works a method was suggested to overcome the lack of signature-based composition currently enabled in component-based and service-oriented architectures (SOA). Several approaches allow to encode non-functional properties of a single component in a contract (component protocol) where the remote calls to a component are taken into consideration. Component protocols ensures that bugs or unsafe behavior caused interaction sequences are obeyed. Encoding business rules works fine as these contracts can be derived from human knowledge only and have to be defined manually, too. In this work we will show, how such unsafe behavior within source code can be discovered and prevented by automatic component protocol generation and model checking techniques.