Overview

BADGER is a tool for correctness verification of software components' behavior specification. The specification, in the form of Threaded behavior Protocols, defines (a) expected usage of each component by other ones, (b) reactions to calls on provided interfaces in terms of methods' invocation on required interfaces, and (c) behavior of internal threads in the case of active components. To get the idea of how the specification in TBP looks like, please navigate to the Example section.

Authors

Tomáš Poch
Ondřej Šerý