Behavioral Consistency Checker


BCC is a model checking based tool to check consistency of UML diagrams. It is developed within the ModelPlex project.

BCC is produced as LIP6 contribution within task 4.3, Model-Based Verification:

  • Software property description metamodel with domain specific property description dialects.

  • Techniques for hierarchical composition of verification models.

  • Verification engines that integrate multiple, concern-specific technologies with different applicability and scope, with heuristics for choosing the most appropriate technology depending on context.

    You can download and run BCC on your project from the download page.