I have released a tool, sbuilder-ethereum
, which translates EthereumSolidiy
language implementations to TLA+.
The idea of the tool is to translate (subset of) a simple language,
such as Solidiy, into formal model, allow users to define correctness
criteria (currently in TLA+ language), allow users to define
environment model aka 'setups' (~tester on steroids acting on the
formal model - and limiting state space explosion). Benefits: increase
confidence to application correctness, and make QA more efficient with
faster feed back.
Current status 'pre-alpha'
* sbuilder-ethereum tool MIT license https://github.com/jarjuk/sbuilder-ethereum
* on-line documentation (translation reference & cucumber tests): http://jarjuk.github.io/sbuilder-ethereum/0.0.6/FEATURES.html
* an overview of the tool in blog post https://jarjuk.wordpress.com/2016/12/08/sbuilder-ethereum-announce
* an example of using the tool https://jarjuk.wordpress.com/2016/12/09/sbuilder-ethereum-example
* for more background information https://jarjuk.wordpress.com/sbuilder/
with a solidity contract and translated TLA result
for one setup. Some benchmark results (using Intel(R) Core(TM) i7-4702MQ CPU @
* generated TLA+ model.tla file 13415 lines long
* 619 states generated, 585 distinct states found, 0 states left on queue.
** generate: real 0m7.757s, user 0m7.600s, sys 0m0.160s
** model checking: real 0m3.863s, user 0m14.722s, sys 0m0.458s
All pointers to similar tools most welcome. Especially would like to see an example, how to document translation semantics.
Next: update road map