Re: [tlaplus] TLA+, Event B comparison

[Michael Leuschel <michael.leuschel@xxxxxxxxx>]

Hello,

I can concur with Stephan’s response.

You may also want to look at our article translating B to TLA+ for applying the TLC model checker to B/Event-B models, which contains some comparisons:
  https://www.sciencedirect.com/science/article/pii/S0167642316300235

A full fledged comparison of B and TLA+ would be an article on its own, made more complicated by the fact that in the B world you have 
 - classical B for software development, supported by the commercial AtelierB prover and its code generators, 
 - and Event-B for systems modelling supported by the open-source Rodin toolset built on top of Eclipse (and also supported by Atelier-B).

Event-B’s events are more rigid than TLA+ actions, while classical B’s operations are quite flexible and allow constructs which do not exist in TLA+.

If code generation is really critical for your application, then you should definitely have a look at “classical B”.
There are code generators available for Event-B, but as far as I know they have not been used for industrial applications yet.

Best regards,
Michael Leuschel

-------------------
For your convenience here is an excerpt from the paper comparing B and TLA+:

B and TLA+ are both state-based formal methods rooted in predicate logic, combined with arithmetic, set theory and support for mathematical functions.
However, as already pointed out in [3],  there are considerable differences:

 B is strongly typed, while TLA+ is untyped.
 For the translation, it is obviously easier to translate from a typed to an untyped language than vice versa. 

 The concepts of modularization are quite different.

 Functions in TLA+ are total, while B supports relations, partial functions, injections, bijections, etc.
 
 B is limited to invariance properties, while TLA+ also allows the specification of liveness properties.

 The structure of a B machine or development is prescribed by the B-method, while in TLA+ a specification, any formula can be considered as a system specification.
 
As far as tool support is concerned, is supported by
 the explicit state model checker and more recently by the TLAPS prover.
 has been used to validate a variety of distributed algorithms (e.g.) and protocols.
B has extensive proof support, e.g., in the form of the commercial product AtelierB and
 the animator, constraint solver and model checker ProB.
Both AtelierB and ProB are being used by companies, mainly in the railway sector for safety critical control software.

-- 
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/F1D32462-7E1B-4342-A8A4-97F17A38878C%40gmail.com.