[SystemSafety] Change cost and (formal) tools

From: David MENTRÉ < >
Date: Mon, 21 Mar 2016 14:00:18 +0100

Hello Roderick,

Le 2016-03-18 17:45, Roderick Chapman a écrit :
> On 18/03/2016 11:00, systemsafety-request_at_xxxxxx > 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:

Best regards,

The System Safety Mailing List
systemsafety_at_xxxxxx Received on Mon Mar 21 2016 - 14:00:30 CET

This archive was generated by hypermail 2.3.0 : Sun Feb 17 2019 - 16:17:08 CET