Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Feedback on presenting Formal Methods

  • Subject: [Frama-c-discuss] Feedback on presenting Formal Methods
  • From: dmentre at linux-france.org (David MENTRE)
  • Date: Mon, 17 May 2010 15:00:12 +0200
Hello,

A few months ago, I asked for help in classifying Formal Methods in
order to present them[1]. I received two very constructive off-list
answers.

I've been asked (by a reader of one of those lists) to report about
the final classification I used. Due to company restriction I cannot
publish my slides however I can outline their content.

I divided my presentation into four main parts:
 * Abstract Analysis (Astr?e, Frama-C, Polyspace);
 * Model checking (SPIN, Scade, ...);
 * Hoare Logic (B Method, Frama-C[2], ...);
 * Interactive Theorem Proving (Coq, PVS, Isabelle, ...).

For each part, I tried to succinctly present the main objectives and
advantages of the presented domain (real code analysis for Abstract
analysis, temporal properties for Model checking, ...) and give a
success story showing how the approach can be interesting (Astr?e for
Abstract analysis, compcert for Interactive theorem proving, ...).
Then, I followed a grid of several points to present the approach,
keeping in mind a very practical point of view (e.g. showing examples
and screen copies of tools):
 * Suitable domains / Possible issues
 * Level of expertise: how the user should be skilled.
 * Level of intervention: hand made model, source code, ...
 * Development cycle coverage / Fidelity: where in the Development
cycle. How to match with real code.
 * Tool availability / Automatism level: are tools available? Automatic ones?
 * Expressiveness: What can be expressed with the considered formalism
(e.g. temporal properties with model checking)

I would like to publicly thank lists' readers that helped me with
ideas and material.

Sincerely yours,
david

[1] http://lists.gforge.inria.fr/pipermail/frama-c-discuss/2010-March/001835.html

[2] Yes, I know, Frama-C is as an Abstract Analysis tool as a Hoare
logic proving tool with Jessie plugin. But it reflected my own usage
and perception of tools availability.