[SystemSafety] Modelling and coding guidelines: software components

Michael J. Pont M.Pont at SafeTTy.net
Thu Mar 17 11:11:58 CET 2016


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 <mailto: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 <mailto:systemsafety at TechFak.Uni-Bielefeld.DE> 




-- 

--

José Miguel Faria

Educed - Engineering made better

t: +351 913000266
w:  <http://www.educed-emb.com/> www.educed-emb.com
e:  <mailto:jmf at educed-emb.com> jmf at educed-emb.com

 

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://lists.techfak.uni-bielefeld.de/mailman/private/systemsafety/attachments/20160317/c920f40a/attachment-0001.html>


More information about the systemsafety mailing list