Abstract
Component based software development techniques are becoming increasingly popular, as they improve the software development process through component reuse. However component based development poses a challenge to software verification: How can we assert the correctness of a black-box component without having access to the internal logic of its implementation? In this paper, we propose an approach to this challenge by validating a component’s communication history with respect to a specification of its observable behaviour using runtime verification techniques. For this purpose we present a simple specification language for describing component behaviour in terms of communication protocols, a language extension to support error handling at the communication level, and a prototype tool to monitor components and assert that they satisfy their protocol specification at runtime. The prototype is implemented for Java components, supports multithreaded access to the monitored components, and is demonstrated on two examples.
