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

[Rene de Visser <rene.de.visser@xxxxxxxxx>]

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/8a7947dc-9b48-45ee-9fd0-d53ffe0b4d9fn%40googlegroups.com.