Abstract
Threaded Behavior Protocols is the newest formalism of the Behavior protocols family for specification of software components' behavior. It features threads, variables, and constructs known from imperative programming languages while still providing strong formal means for verification of composition and refinement.