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

Re: Announcing Sbuilder - a tool to generate TLA+ model for business IT systems



Hello,

I have written a blog entry https://jarjuk.wordpress.com/2016/06/08/sbuilder-roadmap/ with the title "Sbuilder roadmap".

In short, it proposes embedding Sbuilder, a generator to create
specification code in TLA+ language modeling business IT, into an
application framework in order to navigate around resistance involved,
when trying to introduce a separate modeling step to contemporary
software development practices.

I came to the idea after doing some internal trials using current
Sbuilder version: modeling power in TLA+ language is sufficient for my
purposes, and Sbuilder helps in creating specification code for an
implementation.

However, after thinking like a staff manager, who "sees the large
costs involved in building, and maintaining, the capability needed by
the design step", I had to draw the conclusion that pushing an upfront
design like climbing (steep) uphill.


The post does not try to answer the question "how" the embedding
should be done. Instead, it uses current Sbuilder configuration as a
reference, defining what should be extracted from a framework in order
to be able to generate runnable specification model.

The next step, if I were to follow the roadmap proposed, would be to
make an analysis of a candidate framework using the criteria presented in the
post.  Maybe a subject of some future blog entry?

I am interested in pointers to similar approaches.

All comments are most welcome!

BR,

Jukka