This is very interesting - I'm eager to start using it... Does anyone know a quick way to start in a business domain?

At my job, I maintain a well established (read: old) product for moving money. There are a lot of business rules. Formal specification for it all is out of question.

There are though, certain well encapsulated modules which play only a support role -- there is a very faint connection to the core domain, which in this case could easily ignored. One module is a version of "personal task management".

Let's say, the personal task management domain is just being specified. Normally, we'd write in the spec:

* any user has a list of tasks

* any task can have a number of steps

* any step can be started or finished

* user can mark any step as finished or started

* if all steps are finished, the task is closed.

Can anyone help me in expressing these kind of rules in the TLA, please? How could the TLA spec be useful for me?

I find it very interesting to play with, because those "supportive domains" in our product tend to grow quickly and more often than not there comes a change request such as this one:

* the step can have a type (other words: there are two kinds of steps now): manual and automatic.

* all "old" steps are manual steps

* the automatic step is being managed by the application (user cannot change whether it's finished or started)

* the automatic step is executed by some external actor, let's say a process running once a month.

Now, does TLA allow me to "grow the spec" as the requirements come in? Does anyone has this real world, business experience with it (or any other formal specification method) and found it really useful? The example Leslie gave in it's talk (XBox memory bug) seems to be found only by the careful thinking phase and not by TLA directly. Other examples where sorting and finding GCD...

I have no idea how to start using it in my domain. Anyone has the experience (not necessarily with TLA/PlusCalc)?

--- Update

I thought a little bit more to make it closer to what kind of problems we are facing (it's still fictional, so it might not be too coherent).

There comes another change request - the client demands more security! A rule is added:

* any step within the task can be executed only by the same user which added the task to the system.

Now, we have a problem! Automatic processes run with a fake user id ("batch_user_001") and cannot finish the required steps. The user also cannot, since the step is automatic one.

What could we do now? OK, first possibility to explore: use the roles and delegation. Maybe the user should have a role the same as the process? Now the rule could be:

* any step withing the task can be executed only by the user with a role the same as the user adding the task.

Yeah, the tasks can now be processed. OK, but is this the best solution or more of a workaround?

Maybe the process shouldn't run with any user id at all? If I change this part of system how can I check if something else breaks? Like the GUI which assumes "there always IS a user id".

Enough with the fictional scenario. Some conclusions follow.

I believe the formal spec is exactly the tool which would allow to test the interactions of changes more quickly than guessing and/or relying on the expert knowledge (maybe on a sick leave). I be it must be used exactly for the purpose! I considered finding it on my own, but maybe someone here already does it. If yes, kindly please speak up about your experience. :)