Translating B to TLA +  for Validation with TLC

The state-based formal methods B and

TLA

 + 

share the common base of predicate logic, arithmetic and set theory. However, there are still considerable differences, such as the way to specify state transitions, the different approaches to typing, and the available tool support. In this paper, we present a translation from B to

TLA

 + 

to validate B specifications using the model checker

TLC

. We provide translation rules for almost all constructs of B, in particular for those which are not built-in in

TLA

 + 

. The translation also includes many adaptations and optimizations to allow efficient checking by

TLC

. Moreover, we present a way to validate liveness properties for B specifications under fairness conditions. Our implemented translator,

Tlc4B

, automatically translates a B specification to

TLA

 + 

, invokes the model checker

TLC

, and translates the results back to B. We use

ProB

to double check the counter examples produced by

TLC

and replay them in the

ProB

animator. We also present a series of case studies and benchmark tests comparing

Tlc4B

and

ProB

.