Tutorial – McErlang

« back to Presentations Download Presentation Download

In this 90 minute tutorial Lars-Ake Fredlund will introduce the
McErlang model checking tool for verifying Erlang programs, and examine
some case studies where the tool has been successfully applied.

Model
checking is a verification technique where the all the states of a
program are systematically explored and checked against correctness
properties. Although very effective in hardware verification, there are
a number of problems when applying model checking to software:


Need for abstraction: to use a model checking tool it is often
necessary to abstract the source code, almost never is the full source
language supported.

– State spaces are too large for model checking algorithms to work.

In
the design of the McErlang model checker for Erlang we have addressed
both these problems. The language supported is full Erlang, with normal
datatypes, processes, nodes, links, monitors, and so on. Moreover its
verification algorithm provide some answers even when state spaces are
huge (becoming more similar to testing).

Following this
introduction, Clara Benac-Earle will provide a hands-on demonstration
of the tool. Delegates will be shown how to install it onto their
laptops and then they will be taken through some exercises to
demonstrate its usage.

Speakers:

  • Lars-Åke Fredlund

    Erlang researcher and creator of McErlang
    Technical University 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.




    Lars-Åke Fredlund
  • Clara Benac Earle

    Ex-Ericsson CS Lab and model checking expert
    Technical University of Madrid

    Clara was first exposed to Erlang as a student from Spain who got the opportunity to do a master project at Ericsson CSLAB - the birthplace of Erlang. Having seen enough of Sweden, she decided to spread Erlang technology to the UK academy by pursuing a PhD degree at the University of Kent, after which she returned home to Madrid, Spain where she now works at the Technical University of Madrid. Her speciality is model checking Erlang programs, and now works together with other researchers in the European ProTest project on developing new cool Erlang development tools.


    Clara Benac Earle
« back to Presentations

Posted on November 13, 2009

Tags: