BeJC: checking compliance between Java implementation and behavior specification

An important correctness aspect of software built in a modular way is behavior specification of its particular components. Only then one can reason about communication correctness and properties of particular components. Since it is much more effective to do so at the level of behavior models, establishing a correspondence between behavior specification and implementation becomes an important part. In this paper, we present a method for verifying compliance between behavior specification of a software component and its Java implementation. We also discuss practical experience with the BeJC tool that implements the compliance checking algorithm and its application in the software development process.