[marco_salvatori]

You might create a TLA model during the initial specification process to assist you in thinking through your problem. You would then update the model going forward as your understanding of the domain improved and as system requirements changed. However, you could write a specification for an existing system as well. Any processing where the complexity seems greater than ones reasoning ability or that needs assurance guarantees, could signal the need for a high level description to guide engineering efforts.

An initial model might take 4 hours to put in place. The time would be spent thinking through how best to abstract the modeled process and its logical properties, slowly building up a more and more complete set of events, and checking the model by running it as one goes. With an initial model, additional hours would probably be spent here and there adding enhancements and finding ways to do things better, just like one would do with regular code. The model would effectively exist over the lifetime of a corresponding code artifact and guide work on the artifact.

For a standard web application that mostly does reads and writes to a database, there usually wouldn't be any need for a tool like TLA to help you reason. A general use case for TLA is describing systems where there are multiple processes or threads coordinating on some sort of shared state.There would be indeterminacy in the order in which events happen. There could be the possibility of failure and the need to handle it gracefully.

[fulafel]

Web applications can be surprisingly complicated distributed systems, when you take into account..

- the JS frontend that communicates with AJAX and/or WebSockets IPC with the backend

- the backend may actually be a bunch of microservices

- the fact that there are many concurrent frontends (users)

- messages from frontends may end up reordered/dropped/rerouted on their way to different backend ipc channels (microservices or replicated backend)

- the frontends are untrusted (the user or browser may tamper with your code running there)

- the backend server is also often replicated / sharded

- there are caches (think Redis) that the backends share in addition to the main DB.

- load balancers, high-availability reverse proxies with various failover propreties, etc

- various caching behaviours that are only partly under your control (browser-side content caching, DNS, etc)

- all of the above are interconnected over unreliable channels

- there are secrets and security involved so functional assurance ("pressing button X always makes function Y happen") doesn't tell you enough

(I have no TLA+ experience so can't say how one would use it with a web app, though).