Model generation techniques to debug software

International audienceIn this article, we consider the test of synchronous data flow software (written in SCADE) embedded in aircraft computers. The validation of such software is a complex process, which requires some tests in real conditions (e.g. flying conditions). During these tests, some variables of the software are recorded at a chosen frequency. The recorded data represent a partial observation of the state of the computer during the flight. When an unwanted behaviour of the aircraft is detected during the test, we need to identify the cause of this behaviour from the recorded data in order to choose the best way to correct the software. The cause of the observed behaviour can be determined by computing some scenarios consistent with the partial observation according to the specification of the system. The number of plausible scenario might be high and we have to identify a finite subset of the most relevant scenarios. Indeed, each computed scenario involves particular computation paths in the SCADE software. It is worth noting that a computation path can be activated by a class of scenarios. So we propose to compute a scenario per path to identify the part of the software which should be corrected. For these purposes, we have used GATEL tool. We show how to use this tool on an example taken from software of an A320 computer for which the engineers observed the detection of non meaningful alarms, and we compare the result obtained with each tool. For such experiment, the main difficulty is due to a problem of combinatorial explosion, and we show how these tools can take into account the engineer knowledge about the system in order to reduce the number of possible scenarios