Re: [SystemSafety] Modelling and coding guidelines: software components

From: José Faria < >
Date: Fri, 18 Mar 2016 12:16:10 +0000


Michael,

>> Jose,

Do you know how much use has been made of Frama-C in IEC 61508 (or similar) projects?

No. I'm afraid I cannot give a properly substantiated answer. I'd expect the Frama-C "community" to be active at conferences like ERTS2, so I just went into last edition's website <http://www.erts2016.org/>, and indeed found this paper
<http://www.erts2016.org/inc/telechargerPdf.php?pdf=paper_111> under the static analysis topic. The experience report mentions "aeronautical software", but not much further details. Perhaps other people in the list could substantiate further.?

Best,
Jose'

On Thu, Mar 17, 2016 at 10:11 AM, Michael J. Pont <M.Pont_at_xxxxxx wrote:

> Jose,
>
>
>
> I have sympathy with the goal here (use of “task contracts” – with checks
> of pre- and post-conditions - are A Good Thing, in my experience).
>
>
>
> Do you know how much use has been made of Frama-C in IEC 61508 (or
> similar) projects?
>
> All the best,
>
>
>
> Michael.
>
>
>
> Michael J. Pont
>
> SafeTTy Systems Ltd.
>
>
>
> *From:* systemsafety [mailto:
> systemsafety-bounces_at_xxxxxx > Faria
> *Sent:* 17 March 2016 09:48
> *To:* GRAZEBROOK, Alvery N <alvery.grazebrook_at_xxxxxx > *Cc:* systemsafety_at_xxxxxx > *Subject:* Re: [SystemSafety] Modelling and coding guidelines: software
> components
>
>
>
> Alvery,
>
> >Does anyone know of similar annotation schemes on language subsets of C,
> C++ or other more widely used languages?
>
> For C, I'd highlight ACSL, which is supported in the Frama-C platform,
> http://frama-c.com/acsl.html
>
> For C#, there's Spec#, from Microsft,
> http://research.microsoft.com/en-us/projects/specsharp/
>
> For Java, JML,
> http://research.microsoft.com/en-us/um/people/leino/papers/jml-sttt.pdf
>
> Best,
>
> José
>
>
>
>
>
> On Thu, Mar 17, 2016 at 9:22 AM, GRAZEBROOK, Alvery N <
> alvery.grazebrook_at_xxxxxx >
> On the principle of nudging folk in the right direction, it seems to me
> that the use of non-executable annotations (e.g. SPARK) is a valuable
> contribution for defining a library interface contract that would make
> software component re-use more checkable.
>
> Does anyone know of similar annotation schemes on language subsets of C,
> C++ or other more widely used languages? If this concept were to become
> more widely available, it could have a big impact on the expectations for
> "good quality" software components and be used in areas where regulations
> don't reach.
>
> Cheers,
> Alvery
>
> [snip]
> > Whether we like it or not we are all
> >involved in component based design. My experience with software
> >libraries is that there are some good ones out there that are quite
> >stable. On the negative side I have two problems with them:
> >1. They are almost universally very poorly documented so you can waste
> >a day trying to achieve a trivial outcome.
>
> I agree that many examples of software components I have seen have lacked
> sufficient documentation to be able to make sensible decisions about
> suitability. I find that if you can chuck it back via the author to get
> that improved, the documentation improvement is sometimes worthwhile.
> Otherwise you end up writing it yourself.
>
> >2. The authors seem to have no concept of backward compatibility.
> >If you make the mistake of upgrading to the latest version you can
> >trash your complete application: data structure changes, even method
> >name changes. Amazing!#
>
> Regression testing is part of the regimen and any new version has to pass
> all the old tests as well as any new ones. There is a strict notion of how
> much impact changes at lower levels will have on the upper layers of the
> application. I'll happily explain about surfaces to you at some stage.
> [snip]
>
> This email and its attachments may contain confidential and/or privileged
> information. If you have received them in error you must not use, copy or
> disclose their content to any person. Please notify the sender immediately
> and then delete this email from your system. This e-mail has been scanned
> for viruses, but it is the responsibility of the recipient to conduct their
> own security measures. Airbus Operations Limited is not liable for any loss
> or damage arising from the receipt or use of this e-mail.
>
> Airbus Operations Limited, a company registered in England and Wales,
> registration number, 3468788. Registered office: Pegasus House, Aerospace
> Avenue, Filton, Bristol, BS34 7PA, UK.
>
>
> _______________________________________________
> The System Safety Mailing List
> systemsafety_at_xxxxxx >
>
>
>
> --
>
> --
>
> *José Miguel Faria*
>
> *Educed *- Engineering made better
>
> t: +351 913000266
> w: www.educed-emb.com
> e: jmf_at_xxxxxx >
>
>

-- 
--
*José Miguel Faria*
*Educed *- Engineering made better
t: +351 913000266
w: www.educed-emb.com
e: jmf_at_xxxxxx



_______________________________________________ The System Safety Mailing List systemsafety_at_xxxxxx
Received on Fri Mar 18 2016 - 13:16:53 CET

This archive was generated by hypermail 2.3.0 : Fri Feb 22 2019 - 15:17:08 CET