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

Is possible to use TLA+tools to generate test cases on implemenetation


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.

- 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