[SystemSafety] Modelling and coding guidelines: software components

[David Crocker]

For C and C++, there are the annotation schemes used by our own Escher C Verifier and Escher C++ Verifier. See our 2014 conference paper "Can C++ be made as safe as SPARK?" at
http://eschertech.com/papers/CanCPlusPlusBeMadeAsSafeAsSpark.pdf for an overview, and http://eschertech.com/product_documentation/ecvReference/eCv_Manual.html for the details. eCv++ has been used to assist in the verification of safety-critical defence software (to IEC61508 SIL 4) and medical software.

I prefer using a subset of C++ rather than C for critical software development. See http://eschertech.com/articles/items/art100202.html and the following articles in that series for why I think this.

So far as I know, there are no other formal verification tools for subsets of C++. However, there are several other tools for C each with its own annotation scheme, including Microsoft's Vcc, the Jessie plug-in for Frama-C, and VeriFast.

David Crocker, Escher Technologies Ltd.
http://www.eschertech.com
Tel. +44 (0)20 8144 3265 or +44 (0)7977 211486

On 17/03/2016 09:22, GRAZEBROOK, Alvery N 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