[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.