Blog posts

Model checking for the working man


Report written by Steven van Deursen. Thanks!

Wednesday evening, we were invited at in Utrecht for the workshop 'model checking for the working man' by Rico Huijbers.

Soon after start, I was disappointed to discover that the workshop didn't in any way cover fashion super models. Instead the workshop covered tools for developing mathematical proofs for small parts of our software. After recovering from this setback (and after finishing the Wiener schnitzel and French fries provided to us by we opened our laptops for the workshop.

The biggest I took from the workshop was that modeling parts of your software and proving it correct is not something that is purely academic. The tools are freely available and normal developers can learn these tools in a fairly short amount of time. In the workshop we used the tool TLA+ to prove a small piece of code to be thread-safe.

A big plus for me was that Rico was a working man, just like the rest of us. While faced with a multi-threading issue at work, he decided to dive into the world of modeling to see whether a tool could help verifying the correctness of his code. Without any former training and experience he managed to solve that particular issue within a day, which is quite impressive.

Even more impressive is that he did this with the TLA+ tool, because the tool was clearly not built for anything outside the world of academics. The interface was quirky and finding out why the checker reported our model to be invalid gave me a headache!

TLA+ didn't allow debugging the model which made it hard to understand why the model was invalid. This inspired Rico to build his own visualizer using JavaScript which he made available on github. When supplied with the debug output from the model checker, his visualizer allowed showing the steps multiple threads took to get into the invalid state. This gave me a weird mixed feeling of admiration and disgust: admiration for Rico's elegant javascript solution and disgust for the big omission of such a critical feature in TLA+.

The workshop ended with an intriguing discussion between Rico and the participants on whether model checking is actually helpful or not. The main objections were that it was quite tricky to specify a model in such way that it actually correctly resembles the real running code. Converting our code into the model is a delicate matter and can easily go wrong. And after proving our model, converting it back into running code can also go wrong. Besides this, our systems are optimized using a certain memory model, which might be an important to consider while defining the model. Very few developers are really aware of the exact details of such a memory model and reordering of instructions at the compiler and processor level, mixed with latency in processor caching can make it really hard to define a model that even remotely resembles reality. An attendee noted that because of this model checking could even lead to a false sense of security; what does it mean to prove a model is correct while having no way to prove that the model correctly represents the code?

I enjoyed the workshop and Rico's has a very pleasant way of presenting. Rico gave me food for thought, but in the end, Rico wasn't able to convince me to try model checking. This was due to a combination of the TLA experience mixed with the identified risks of inaccurately specifying the model.

Let’s hope that in the near future we see improved tooling and integration of tools into our normal development environments so that real code can be proven. When that happens we can truly say that model checking has become feasible for the working man.

Did you miss the workshop? All material is available online! Model checking for the Working Man (m/f)


Subscribe to our newsletter

Newsletter archive

News @devnologynl

#devnology meetup: Trench Talk - Models and friends with @yreynhout, Nov 25 at @AvivaSolutions in Koudekerk ad Rijn

23-10-2015 at 17:40

Missed tonight’s meeting by @rix0rrr at @bol_com? Material is available online: /cc @mgilbir

21-10-2015 at 19:09

RT @DavyLandman: Now at @devnologynl @rix0rrr explains how he picked up TLA+ and profited within a few hours. A win for modeling community.

21-10-2015 at 16:59


Processing workshop

Domain modelling with the F# type system: Make illegal states unrepresentable

Learn a new language: Pharo

Codefest Algoritmiek

Community Day 2014 Schedule

Devnology Community Day 2014!

Back to School: Static versus dynamic typing

Report Meten is weten

Report Devnology weekend 2013

Back to School - Software operation knowledge

Kids Programming Lego Mindstorms

Conferentie Software Development Automation 2013 op 29 mei 2013

Auteursrecht en Open Source

Free talk with Philippe Kruchten

Report Global Day of Coderetreat AMS 2012

Verslag Back to School - Software security

October Amsterdam Clojure Event

A journey to Arduino for a Java programmer

Report Learn a language : LISP

Visual Studio 2012 Launch event

Coderen mét Corey Haines

Verslag Back to School - Zin en onzin van modeleren

Moving forward

Report CodeFest Space Invaders

Review Community Day 2012

Community Day 2012 report

Verslag Ignite Talks Night

Why our next event is not a Pecha Kucha night

Global Day of Coderetreat 2011

Verslag Back to School IV - Agility en Architectuur

Verslag Back to School III : Software impact

Amsterdam Erlang Factory Lite

GoTo Amsterdam 2011

Verslag Open Space 2011

Programma Open Space 2011

Report - Back to School II - software re-engineering using visualization

Verslag Back to School: de Software vulkaan

Verslag Legacy code fest - Pong!

Report - The Kata in the Hat

Workshop Genetisch Programmeren

Verslag Coding Dojo TSP

Verslag Retrospective 2010

Presentaties Community day 2010

Community Day 2010: Socializen, kennisslurpen en antischaap

Verslag Community Day 2010

Installatieinstructies workshops Community day

Verslag Devnology weekend 2010

Agenda Community Day 2010

Fitnesse workshop

Community day 2010, call for content

Verslag DNSSEC: Internet achter de schermen

Verslag Open Space 2010

Programma Open Space 2010

Verslag code inspectie met IfSQ

Verslag Tetris codefest

Verslag Rascal workshop

Follow-up Pacman kata

Verslag Coding Dojo

Verslag Retrospective 2 december 2009

Presentaties Community Day

Dé favoriet:

Aviva Solutions sponsort Code Fest

Je favoriete ..

Devnology, a bridge between developer communities

About Programmer Lifestyle Dilemmas

Verslag Ronde Tafel bijeenkomst 6 mei 2009

Python en de Google AppEngine op het Code Fest

Video impressie van de Software Testing Middag

Verslag Code Fest 1 april 2009

Verslag gastcollege TU Delft 25 maart 2009

Qwan 5dff39510bacfcefb54e89f953eddfc1a7a21185b7128d96ff6b466f56acb6d9
Macaw 06e9331a5321067b592bf45ea39db7df6792dc976000d24d3ee4043d99203514
Finalist e304343cdbeb0996cc1e7a26527993a5fa2db87ca53a81fb15dca22a35d7f28c

Devnology is a non-profit organisation and thus depends on sponsors. Thanks to our wonderful sponsors all Devnology events are free!