Modelling a REST API server in TLA+ - suggestions/examples

[bpr...@hotmail.com]

Hello,

I am trying to model a REST API server in TLA+. It's my first attempt at using a formal language and TLA+; I'm finding it challenging to abstract things like a database/storage or user credentials.

I have tried to find any materials on modelling this sort of system in TLA+, but I've been unable to find any. If anyone here has any examples or suggestions on how to go about this, it would be greatly appreciated! I can give additional details if required.

Thanks

[LUMING DONG]

First, you should produce the finite state machine according to the logical architecture of your system, which usually described by UML interaction and State diagrams.

Then try to define the state variables of each objects in the interaction course, which can be obtained by refinning the key attributes of the corresponding classes.

So far, you will get a vivid description in your mind about how the state machine of each object transited according to the interactions, 

now you can easily depicts this event driven discret system by TLA+.

You can get some exmaple from Specifying System