--- layout: fc_discuss_archives title: Message 59 from Frama-C-discuss on May 2010 ---
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.