TLA+ for beginners

[Abay]

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

[Ioannis Filippidis]

On Friday, November 25, 2016 at 5:12:17 AM UTC-8, Abay Kozhabergenov wrote:

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.

Hi Abay,

You may want to look at [1] and [2]. There are also some posts in this Google group with relevant comments that
can be found by searching for "real time" at the top, for example [3].

[1] https://research.microsoft.com/en-us/um/people/lamport/pubs/pubs.html#real-simple
[2] Ch.9 in the TLA+ book, https://research.microsoft.com/en-us/um/people/lamport/tla/book.html
[3] https://groups.google.com/d/msg/tlaplus/uw7ZtLVQPLo/bw3_BKGeFAAJ

Best regards,
ioannis

[Markus Alexander Kuppe]

On 25.11.2016 14:11, Abay wrote:
> I downloaded the TLA+ toolbox, but there I could not find, for
> example, "create new project" option in menu bar.

Hi Abay,

I've made a very basic TLA+ Toolbox for Beginners screencast [1] to help
you get started.

Cheers
Markus

[1] https://vimeo.com/193107865

[Markus Alexander Kuppe]

On 25.11.2016 23:33, Markus Alexander Kuppe wrote:
> Hi Abay,
>
> I've made a very basic TLA+ Toolbox for Beginners screencast [1] to help
> you get started.
>
> Cheers
> Markus
>
> [1] https://vimeo.com/193107865

Youtube seems superior to Vimeo ~> https://youtu.be/U2FAnyPygrA has
captions.

M.