Runtime Validation of Communication Histories

Component based software development techniques are becoming increasingly popular, as they improve the soft- ware development process through component reuse. How- ever 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 in- ternal logic of its implementation? In this paper, we pro- pose an approach to this challenge by validating a compo- nent's communication history with respect to a specifica- tion of its observable behaviour using runtime verification techniques. For this purpose we present a simple specifica- tion language for describing component behaviour in terms of communication protocols, a language extension to sup- port error handling at the communication level, and a pro- totype tool to monitor components and assert that they sat- isfy their protocol specification at runtime. The prototypeis implemented for Java components, supports multithreaded access to the monitored components, and is demonstrated on two examples.