Abstract
BeJC is a tool for checking consistency between component implementation in Java and specification in the language of Threaded Behavior Protocols (TBP). Behavior specification of a component in TBP defines sequences of method calls that the component must handle (i.e., permitted usage of the component) and also sequences of calls that each method is allowed to perform.
The component's implementation is consistent with the specification if it responds to all permitted calls on its interfaces in a way allowed by the specification.