[SystemSafety] Change cost and (formal) tools

[David MENTRÉ]

Hello Roderick,

Le 2016-03-18 17:45, Roderick Chapman a écrit :
> On 18/03/2016 11:00, systemsafety-request at lists.techfak.uni-bielefeld.de
> wrote:
>> The only issue with this approach is the cost and the technical
>> complexity. A very few organisations are ready to pay that cost.
> David,
>  I'm not sure what you mean by those points.
> 
> What cost? Of tools or training?

Cost of tool is not negligible (it is the first cost seen) but training
costs and more over social impact on current processes (change of user
habits) are mostly problematic.

> Do you have any data
> to support that? 

Unfortunately not.

> What reduction in defect density (and thus
> downstream cost saving in other verification activities and re-work)
> is required to justify adoption of a more formal approach?

I think if you can show management a *COST* reduction of 10% or even 5%,
it would be enough. I'm strongly emphasizing the "cost" term. Management
can understand defect density and similar notions, but at the end of the
day, only monetary cost is looked at.

> My experience is that almost no organisations have such data,
> and therefore can't just justify the RoI argument to change their
> ways.  The default behaviour is "do the same as last time, but promise
> to be more careful" ... even if "last time" was a horrible mess.

You are precisely right. Nobody has such data, so it is very difficult
to justify a new approach (being formal, model based or any other tool).
So people are keeping the same, old and sometimes bad habits. I strongly
agree with you.

If you can show an impact on the reduction of number of tests, it could
be understood by management. Do you have such figures for SPARK?

> What's "technical complexity" mean?  Of what?

The complexity to learn new formalism, languages, set of tools, etc. In
my company, they have C programmers and apparently they don't want to
change anything. And people are overwhelmed with work, so no "free time"
to learn or even get interested to new things.

In a business unit of my company, they looked at both B Method and SCADE
(because client is requesting formal methods). B Method was rejected on
the (true) basis of complexity, even if you can find public data
confirming B Method can be cost effective and produce high quality
systems. SCADE is trialed, its graphical approach having a good effect
on management. But SCADE nice diagrams are hiding the complexity of
doing an efficient synchronous program. I also suggested SPARK, but it
was rejected (see below).

> I imagine Frama-C suffers from all the same adoption hurdles as
> SPARK, possibly worse in some areas. For example - Frama-C requires
> _more_ user-added contracts than SPARK to make up for the deficiencies
> in C's underlying type system.

Yes, for now I don't even try to sell Frama-C internally, except for
Value analysis plug-in where you have very little annotations to add.
But even with such a tool that has low impacts on current development
process, it is very difficult to get it adopted.

Regarding SPARK, I fully agree that SPARK seems to me much more
manageable than Frama-C / WP if you want to go on the code proof path.
But in an organization like mine, you have major hurdles:

 * Changing habits of programmers, adopting a total new language! Even
if Ada is not far from C for the basic core of Ada (compared to OO,
functional or synchronous languages). Sadly, people don't look beyond
the fact that the word "Ada" is different from "C";

 * The existing code base. Yes, I know, you can easily link Ada with C.
But then you'll have two code bases in two different languages.

Best regards,
david