[SystemSafety] Modelling and coding guidelines: software components

[André Passos]

Hi Michael,

In the context of IEC 61508 I don't know but there is a nice article in
DO-178C context (
http://www.open-do.org/wp-content/uploads/2013/04/IEEE_Software_Formal_Or_Testing.pdf
).

Regards, Andre.

2016-03-17 11:11 GMT+01:00 Michael J. Pont <M.Pont at safetty.net>:

> 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
>
>
>
> _______________________________________________
> The System Safety Mailing List
> systemsafety at TechFak.Uni-Bielefeld.DE
>
>


-- 
Cumprimentos, André Passos.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://lists.techfak.uni-bielefeld.de/mailman/private/systemsafety/attachments/20160317/535e5856/attachment.html>