Developing reliable concurrent software is a hard task given the inherent non-deterministic nature of concurrent systems. A technique which is often used to check that a concurrent program fulfils a set of desirable properties is model checking. In model checking, all the states of a concurrent system are systematically explored.
McErlang is a tool which helps finding bugs in concurrent Erlang programs using model checking. In this tutorial we
will illustrate the use of McErlang through simple examples.
A new functionality is the integration of QuickCheck and McErlang; we show how the same QuickCheck state maching model can be checked either using QuickCheck, QuickCheck/Pulse or QuickCheck+McErlang, and explain the trade-offs of using the tools.
Lars-Åke FredlundErlang researcher and creator of McErlang
Universidad Politécnica of Madrid
Lars-Ãke first learned of Erlang when attending a course on "Declarative Real-Time Programming" at the Royal Institute of Technology in 1991. Working at the Swedish Institute of Computer Science (SICS), the relationship with Erlang continued; one outcome was a formal semantics for Erlang (part of his PhD thesis in 2001). Lured to Madrid in 2005, Lars-Ãke found more free time to work with Erlang resulting in a number of articles concerning the "real" communication guarantees of Erlang (more tricky than you think...) and a cool new tool to verify concurrent Erlang software: McErlang. He also tries, mostly in vain, to convince his office mates and students at the Technical University of Madrid that Erlang has a much better process model than ADA.