A number of logical code coverage criteria have been used throughout the years in the testing of safety-critical software. Kaminski, et al. proposed Relational Operator Replacement Global (RORG), a method to bring benefits from ROR mutation to Modified Condition / Decision Coverage (MCDC), which is widely used in the avionics industry. However, there is a lack of studies in the industry to support this method. In this thesis, we report on the results of applying RORG to avionic code, augmenting an MCDC adequate test set to satisfy RORG, evaluating its ability to find real faults in industrial software. Conclusions drawn from this thesis are: (1) Faults in relational operators in avionic code are rare, no faults were found in this study. (2) 24% of the relational operators in our study would require additional software requirements to be verified for RORG coverage. (3) 37% of the relational operators in our study were infeasible to test due to program semantics. (4) 84% of the tests added covered enumeration comparisons.

This work describes the process of the design of a flight software for a space-qualified device, outlines the development and testing of the SW, and provides a description of the final product. The flight software described in this work has been developed for the project Demise Observation Capsule (DOC). DOC is a device planned to be attached to an upper stage of a launch vehicle and observe its demise during atmospheric re-entry at the end of its mission. Due to constraint on communication time during the mission and the need to maximize the amount of transferred data, a custom communication protocol has been developed. / Demise Observation Capsule

Les logiciels critiques nécessitent l’obtention d’une évaluation de conformité aux normesen vigueur avant leur mise en service. Cette évaluation est obtenue après un long travaild’analyse effectué par les évaluateurs de logiciels critiques. Ces derniers peuvent être aidéspar des outils utilisés de manière interactive pour construire des modèles, en faisant appel àdes analyses de flots d’information. Des outils comme SPARK-Ada existent pour des sous-ensembles du langage Ada utilisés pour le développement de logiciels critiques. Cependant,des langages émergents comme ceux de la famille ML ne disposent pas de tels outils adaptés.La construction d’outils similaires pour les langages ML demande une attention particulièresur certaines spécificités comme les fonctions d’ordre supérieur ou le filtrage par motifs. Cetravail présente une analyse de flot d’information pour de tels langages, spécialement conçuepour répondre aux besoins des évaluateurs. Cette analyse statique prend la forme d’uneinterprétation abstraite de la sémantique opérationnelle préalablement enrichie par desinformations de dépendances. Elle est prouvée correcte vis-à-vis d’une définition formellede la notion de dépendance, à l’aide de l’assistant à la preuve Coq. Ce travail constitue unebase théorique solide utilisable pour construire un outil efficace pour l’analyse de toléranceaux pannes. / Critical software needs to obtain an assessment before commissioning in order to ensure compliance tostandards. This assessment is given after a long task of software analysis performed by assessors. Theymay be helped by tools, used interactively, to build models using information-flow analysis. Tools likeSPARK-Ada exist for Ada subsets used for critical software. But some emergent languages such as thoseof the ML family lack such adapted tools. Providing similar tools for ML languages requires specialattention on specific features such as higher-order functions and pattern-matching. This work presentsan information-flow analysis for such a language specifically designed according to the needs of assessors.This analysis is built as an abstract interpretation of the operational semantics enriched with dependencyinformation. It is proved correct according to a formal definition of the notion of dependency using theCoq proof assistant. This work gives a strong theoretical basis for building an efficient tool for faulttolerance analysis.

The importance and requirements of certifying safety critical software is today more apparent than ever. This study focuses on the standards and practices used within the avionics, automotive and medical domain when it comes to safety critical software. We identify critical problems and trends when certifying safety critical software and propose a proof-of-concept using static analysis, model checking and incremental SAT solving as a contribution towards solving the identified problems. We present quantitative execution times and code coverage results of our proposed solution. The proposed solution is developed under the assumptions of safety critical software standards and compared to other studies proposing similar methods. Lastly, we conclude the issues and advantages of our proof-of-concept in perspective of the software developer community