TLA+ for beginners

[Abay <abay.kozh...@xxxxxxxxx>]

Hi everyone,

I am working in a company which develops different kinds of software. Our new project is to develop a software for the interlocking system, which controls rail systems. The software is written using the state-machine (blocks) language (very simple) which is provided by a PLC devices provider. I am a new worker in the Verification and Validation Department. Consequetly, it is necessary to verify the software parts, for example, controlling pointer machine etc. All parts of the software use pretty simple operations such as arithmetical operations, boolean logic etc. The hardest part is that some parts have timer block which, as I know, can be modelled only in TLA+, not in LOTOS, B method's Event-B etc. 

So, can you help how to begin the model checking and the formal proof for my case in TLA+, please?

 Good tutorial will be very useful. I downloaded the TLA+ toolbox, but there I could not find, for example, "create new project" option in menu bar. 

Best regards...

Abay