Ethereum Meetup Helsinki Presentation 8th March 2017

This post contains slides for a presentation on Sbuilder model checking performance, held on the 8th March 2017 in Ethererum Meetup Helsinki.

Fin

The slides present benchmark results of TLA+tools model checker performance, as a number of states processed per second, when model checking a formal model generated by sbuilder. For controlling number of states in a state space refer to Heuristics Used in Creating Runnable Formal Models.

Benchmarks indicate that model checking is CPU bound, and heavily influenced by code volume in the formal model.

For scaling to real world applications the blog entry suggests 1) model checking application in chunks, and 2) distributing model checking tasks to several workers, 2a) using multiple cores in a CPU, or 2b) running on a distributed hardware.

Preparing a blog entry, which gives more details of the results, and an their impact on sbuilder roadmap v2.

Advertisements

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s