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

From: David MENTRE < >
Date: Thu, 17 Mar 2016 14:57:58 +0100


Le 17/03/2016 10:22, GRAZEBROOK, Alvery N a écrit :
> 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?

B Method is not a widely used language but has a similar annotation scheme. It is used widely throughout the world by Siemens and Alstom for their CBTC (Communication Based Train Control) and (railway) Interlocking projects (see It allows to re-use and adapt the software to a new context while knowing precisely what your are breaking.

Coming back to a previous point in a discussion, formal contracts (i.e. what your are calling non-executable annotations) is a way (the only way?) to precisely define what is the "environment" (i.e. the assumptions) of your program and know when you can re-use it or not.

The only issue with this approach is the cost and the technical complexity. A very few organisations are ready to pay that cost. I think some lest powerful approaches but less costly could be more widely used.

Best regards,

The System Safety Mailing List
systemsafety_at_xxxxxx Received on Thu Mar 17 2016 - 14:58:05 CET

This archive was generated by hypermail 2.3.0 : Tue Jun 04 2019 - 21:17:08 CEST