Toward a cooperative and open framework for the development of certifiable software

Last time I met John Chilenski at the SC-205 (DO-178C) working group, I mentioned to him the concrete and theoretical results of the couverture project. Since our work had been partly inspired by the research studies he worked on for the FAA (http://www.faa.gov/aircraft/air_cert/design_approvals/air_software/research), I was convinced that our results would be of interest to him. I suggested that he take a look at the paper we published at ERTS 2010 (http://www2.adacore.com/wp-content/uploads/2010/06/couverture_ertss2010.pdf) and he came back with an interesting question:

‘Hi Cyrille,

I hope you had a Merry Christmas and a Happy New Year!

I have a question for you. In the paper you state: “When some conditions involve multiple conditional branch instructions, OBC still implies MC/DC, but becomes in effect an even stronger property: MC/DC could potentially be established by a test set that does not achieve OBC.”

When does a condition involve multiple conditional branch instructions? I would appreciate an example to help me understand this.

Thanks,

-John’

to which I answered:

‘the code generator may have to generate multiple conditions for various constructs of a language depending on what this construct does. For instance, in Ada :

if Table (I) > 3 then

there is clearly a single condition here but if checks are enabled, the object code for this condition will contain additional branches because of the index check. Basically anything that is supposed to be detected by a good Source-to-Object traceability analysis as “non immediately traceable” is a likely candidate. another example that doesn’t involve Ada dynamic checks:

if (A mod B) = 0 then ….

if you look at the code generated by such a sequence, you might be surprised by the number of conditionals that might be generated for such a trivial expression ’