[SystemSafety] Modelling and coding guidelines: software components

José Faria jmf at educed-emb.com
Fri Mar 18 13:16:10 CET 2016


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 safetty.net>
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 lists.techfak.uni-bielefeld.de] *On Behalf Of *José
> Faria
> *Sent:* 17 March 2016 09:48
> *To:* GRAZEBROOK, Alvery N <alvery.grazebrook at airbus.com>
> *Cc:* systemsafety at lists.techfak.uni-bielefeld.de
> *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 airbus.com> wrote:
>
> 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 TechFak.Uni-Bielefeld.DE
>
>
>
>
> --
>
> --
>
> *José Miguel Faria*
>
> *Educed *- Engineering made better
>
> t: +351 913000266
> w: www.educed-emb.com
> e: jmf at educed-emb.com
>
>
>



-- 
--
*José Miguel Faria*
*Educed *- Engineering made better
t: +351 913000266
w: www.educed-emb.com
e: jmf at educed-emb.com
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://lists.techfak.uni-bielefeld.de/mailman/private/systemsafety/attachments/20160318/fc67d866/attachment.html>


More information about the systemsafety mailing list