Formal Guaranties for Safety Critical Code Generation: the Case of Highly Variable Languages

Les fonctions de commande et de contrôle sont parmi les plus importantes des systèmes embarqués critiques utilisés dans des activités telles les transports, la santé ou la gestion de l’énergie. Leur impact potentiel sur la sûreté de fonctionnement fait de la vérification de leur correction l’un des points les plus critiques de leur développement. Cette vérification est usuellement effectuée en accord avec les normes de certification décrivant un ensemble d’objectifs à atteindre afin d’assurer un haut niveau de qualité du système et donc de prévenir l’apparition de défauts. Cette vérification du logiciel est traditionnellement basée sur de nombreux tests et des activitiés de relectures de code, toutefois les versions les plus récentes des standards de certification permettent l’utilisation de nouvelles approches de développement telles que l’ingénierie dirigée par les modèles et les méthodes formelles ainsi que l’utilisation d’outil pour assister les processus de développement. Les outils de génération automatique de code sont exploités dans la plupart des processus de développement de systèmes embarqués critiques afin d’éviter des erreurs de programmation liées à l’humain et pour assurer le respect des règles de production de code. Ces outils ayant pour vocation de remplacer les humains pour la production de code, des erreurs dans leur conception peuvent causer l’apparition d’erreurs dans le code généré. Il est donc nécessaire de vérifier que le niveau de qualité de l’outil est le même que celui du code produit en s’assurant que les objectifs spécifiées dans les normes de qualification sont couverts. Nos travaux visent à exploiter l’ingénierie dirigée par les modèles et les méthodes formelles pour développer ces outils et ainsi atteindre un niveau de qualité plus élevé que les approches traditionnelles. Les fonctions critiques de commande et de contrôle sont en grande partie conçues à l’aide de langages graphiques à flot de données. Ces langages sont utilisés pour modéliser des systèmes complexes à l’aide de blocs élémentaires groupés dans des librairies de blocs. Un bloc peut être un objet logiciel sophistiqué exposant une haute variabilité tant structurelle que sémantique. Cette variabilité est à la fois liée aux valeurs des paramètres du bloc ainsi qu’à son contexte d’utilisation. Dans notre travail, nous concentrons notre attention en premier lieu sur la spécification formelle de ces blocs ainsi que sur la vérification de ces spécifications. Nous avons évalué plusieurs approches et techniques dans le but d’assurer une spécification formelle, structurellement cohérente, vérifiable et réutilisable des blocs. Nous avons finalement conçu un langage basé sur l’ingénierie dirigées par les modèles dédié à cette tâche. Ce langage s’inspire des approches des lignes de produit logiciel afin d’assurer une gestion de la variabilité des blocs à la fois correcte et assurant un passage à l’échelle. Nous avons appliqué cette approche et la vérification associée sur quelques exemples choisis de blocs issus d’applications industrielles et l’avons validé sur des prototypes logiciels que nous avons développé. Les blocs sont les principaux éléments des langages d’entrée utilisés pour la génération automatique de logiciels de commande et de contrôle. Nous montrons comment les spécifications formelles de blocs peuvent être transformées en des annotations de code afin de simplifier et d’automatiser la vérification du code généré. Les annotations de code sont vérifiées par la suite à l’aide d’outils spécialisés d’analyse statique de code. En utilisant des observateur synchrones pour exprimer des exigences de haut niveau sur les modèles en entrée du générateur, nous montrons comment la spécification formelle de blocs peut être utilisée pour la génération d’annotations de code et par la suite pour la vérification automatique des exigences. Finalement, nous montrons dans quelle mesure les spécifications de blocs permettent de générer des données de qualification tel que des exigences, des tests ou des données de simulation utilisées pour la vérification et le développement de générateurs automatiques de code. ABSTRACT : Control and command softwares play a key role in safety-critical embedded systems used for human related activities such as transportation, healthcare or energy. Their impact on safety makes the assessment of their correctness the central point in their development activities. Such systems verification activities are usually conducted according to normative certification guidelines providing objectives to be reached in order to ensure development process reliability and thus prevent flaws. Verification activities usually relies on tests and proof reading of the software but recent versions of certification guidelines are taking into account the deployment of new development paradigms such as model-based development, and formal methods; or the use of tools in assistance of the development processes. Automatic code generators are used in most safety-critical embedded systems development in order to avoid human related software production errors and to ensure the respect of development quality standards. As these tools are supposed to replace humans in the software code production activities, errors in these tools may result in embedded software flaws. It is thus in turn mandatory to ensure the same level of correctness for the tool itself than for the expected produced code. Tools verification shall be done according to qualification guidelines. We advocate in our work the use of model-based development and formal methods for the development of these tools in order to reach a higher quality level. Critical control and command software are mostly designed using graphical dataflow languages. These languages are used to express complex systems relying on atomic operations embedded in blocks that are gathered in block libraries. Blocks may be sophisticated pieces of software with highly variable structure and semantics. This variability is dependent on the values of the block parameters and of the block's context of use. In our work, we focus on the formal specification and verification of such block based languages. We experimented various techniques in order to ensure a formal, sound, verifiable and usable specification for blocks. We developed a domain specific formal model-based language specifically tailored for the specification of structure and semantics of blocks. This specification language is inspired from software product line concepts in order to ensure a correct and scalable management of the blocks variability. We have applied this specification and verification approach on chosen block examples from common industrial use cases and we have validated it on tool prototypes. Blocks are the core elements of the input language of automatic code generators used for control and command systems development. We show how our blocks formal specification can be translated as code annotations in order to ease and automate the generated code verification. Code annotations are verified using specialised static code analysis tools. Relying on synchronous observers to express high level requirements at the input model level, we show how formal block specification can also be used for the translation of high level requirements as verifiable code annotations discharged using the same specialised tooling. We finally target the assistance of code generation tools qualification activities by arguing on the ability to automatically generate qualification data such as requirements, tests or simulation results for the verification and development of automatic code generators from the formal block specification