Hello,
I have been developing a tool called
sbuilder, which produces formal models in TLA+ language
representing "business IT" systems, i.e. application with interfaces, persistent state and
service semantics between these two.
The idea is to use a formal model to generate "virtual system tests". The work flow:
1) Create a formal model + with correctness invariant (assisted by sbuilder translation)
2) Run model checking on formal model in the "usual" way
3) Run model checking using a configuration, which produces a counter example,
which represent execution we would like to test the system with.
4) Parse the counter example and extract interface calls steps: a) state of the formal model
before interface call, b) formal model parameter binding to the interface call, c)
formal model interface response message, d) formal model state after the call
5) iterate each interface step in the trace and execute it as unit test
a) map formal model before state to implementation state && init SUT with that state
b) map formal model interface parameter bindings to a request in implementation state && send that req. msg to SUT
c) recieve response msg from SUT and compare it with formal model response message mapped to implementation state
d) map formal model after state top implementation && check SUT state
6) Interpret the aggregate result of executing individual unit tests as a virtual system test
As the result:
- expect saving in "virtual" system testing, because executing unit test is considerable easier than trying to
manage execution of a system test as a single unit
- formal model and imlementation conformance increased
For more details ref
Specification Driven Development , for a
demo.
To create a counter examples, referenced above, sbuilder offers "possibility" operators, which are implemented
on top of TLA+tools extension feature. A possibility operator translates to an extension module, which extends base module holding
formal model of the application. The extension module requires negation of "possibility" operator to hold universally.
In step 2 above, we would be model checking using the base module, and in step 3,
using the extension module. Refer to an
example in a blog entry for more details.
Questions:
- Is the idea to use invariant to generate test cases "kosher"?
- How about the possibility operator is a LTL formula with UNTIL operators, could it still be prefixed with [] ~
and use to generate counter example demonstrating that state represented by the possibility operator can
be reached?
Best Regards, Jukka