Tag - B-method

Entries feed - Comments feed

Last entries

Introduction aux méthodes formelles actualisée

Comme en 2010 et 2011, j'ai faire une intervention de 2h pour présenter les méthodes formelles à l'ESIR, école d'ingénieur de Rennes 1. J'ai un peu actualisé la présentation, je pense qu'elle est plus illustrée et j'ai introduit quelques démonstrations d'utilisation des outils. La présentation est disponible en PDF ou en source au format PowerPoint (licence Art Libre, sauf pour les illustrations, que j'ai pioché à droite et à gauche sur le web).

Note pour les libristes : la plupart des logiciels mentionnées sont libres.

How to install Atelier B 4.1 on a Debian-like 64 bits machine

Atelier B 4.1 has just been released. For Linux machines, it is available as a binary packages for 32 bits x86 machines in RPM and DEB format. Unfortunately the DEB package won't work on a Debian-like 64 bits machine, for example an Ubuntu. Here the approach have I used to install the package:

Install Atelier B 4.1 in /opt/atelierb-4.1

  • mkdir /tmp/ab
  • cd /tmp/ab
  • wget http://www.atelierb.eu/atelier-b/4.1/free/AtelierB-4.1.0-free-linux.deb
  • ar xv AtelierB-4.1.0-free-linux.deb
  • cd /
  • sudo tar zxf /tmp/ab/data.tar.gz
  • sudo chown -R YourUserID:YourGroup /opt/atelierb-4.1/ # substitute YourUserID and YourGroup with adequate values

Configure the execution environment on an Ubuntu 12.04

  • sudo apt-get install ia32-libs-multiarch

You can now start Atelier B with:

 /opt/atelierb-4.1/startAB &

The procedure might be different for another Debian-like distribution, including Debian itself. You can add specific procedures for a given distribution in the comments.

Which approach for Hoare logic formal verification?

Currently, if one wants to do some program verification using Hoare logic framework, three approaches are possible:

  1. Down to code approach, when one annotates code functions with pre and post-conditions. This is the approach proposed by Frama-C on C code, SPARK on Ada code or GNATprove on Ada code. This approach has the advantage to be directly palatable to programmers because they are keeping they preferred language. Moreover, one can use such approaches on existing code, even if to fully verify it one will probably need to make some change. The downside of the approach is that the formal verification is tightly linked to the code, making the formalisation of program wide properties more complex;
  2. Abstract specification refined in implementable code, like the B Method (and its variant Event B for system specification). This approach using using pre and post-conditions but also invariants on which all the correctness of the code is built. Due to its abstract specification, it can express complex properties that help reasoning on the built program or system. However, it uses very mathematical concepts like set theory or relations which are making engineers not at ease. And the proof can be somewhat complex, involving some manual steps. Moreover, one needs to fit its development process in B approach, without reuse of existing code;
  3. A new approach proposed by Bertrand Meyer (of Eiffel fame which popularized the Design by Contract approach) which relies on pre and post-conditions on code but where such specification can use more abstract operators made available from libraries called Domain theories. The main idea is that such domain theories provide to the programmer abstract view on some domains (like maximum of an array) so formal specifications are easier to read (and thus probably more correct) and hopefully to prove.

The third approach of Meyer seems to take most advantages of the two first ones: use of current programming language so the programmer is at ease and use of abstract formalisation so the specification is easier to read and more abstract. Moreover, it relies heavily on invariants (already available in Eiffel language) so a B Method-like approach is possible. However, Meyer's approach lacks refinement capabilities of B Method. But as far as I know, refinements are rarely used in B Method, except for making difficult proofs easier by using several steps to make concrete algorithms or data structures[1].

It remains to see how it will be implemented in a tool. Formal methods effective capabilities are determined by the supporting tools. Time will tell if Meyer's approach is really useful! :-)

Note

[1] But that might make the difference between a nice approach and a usable one. ;-)