[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[tlaplus] Modeling an object oriented design



There used by a modeling language called  LePUS3 (https://en.wikipedia.org/wiki/LePUS3) which was used to formally model object oriented design.  It was popular in 2000s  but seems to have disappeared about 10 years ago. 

With that I am exploring using TLA+ for formally modeling an object oriented design. 
The way I see it should be workable solution.

Class/Object are represented as data structure , I think we call them record in TLA+.

Define transition rules that will mutate this object. 

So far, I am still pondering how to model a class instantiation as in creation of an object from class. I guess if it is singleton pattern, it wouldn't matter. 

My goals:
to start with      -Use TLA+ as tool to understand complex object oriented design
Next step-Try modeling checking some invariants.
Would be nice- To visualize the model in some form of diagram. 

What I am looking for:
Is TLA+ suitable for object oriented modeling/specification. Is there precedent for this application?  




--
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 on the web visit https://groups.google.com/d/msgid/tlaplus/32d0d40d-11d8-4fe7-942d-75613e4358fen%40googlegroups.com.