[tlaplus] Re: Modelling application: reuse modules for database access and processes?

[Andrew Helwer <andrew.helwer@xxxxxxxxx>]

It's hard to make general models of this sort to build on top of because what you actually care about modeling varies quite a bit from case to case. However I agree it would be nice to have an organized series of models that work decently well as external views of various common systems. Not likely to happen in the near future unless someone wants to put in the work though.

Andrew

On Tuesday, November 5, 2024 at 11:58:16 AM UTC-5 Rene de Visser wrote:

I am thinking of modelling part of a (business) application in TLA+ .

The application runs concurrently in multiple processes and concurrently accesses a SQL database with the standard row level locking, MVCC and isolation.

It looks like modelling the application is a doable amount of work, but modelling the database and OS processes, with locks, wait queues, time outs, deadlock detection, etc is a lot of work.

I wonder that I haven't yet found TLA+ modules that model the standard OS and DB parts so that a I can use them and just model the application part?

Best regards,

Rene.

-- 
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 visit https://groups.google.com/d/msgid/tlaplus/02508391-5f35-444f-8747-0d2a56cb6f9cn%40googlegroups.com.