Search

Over the past two decades, the promoters of Model Based Systems Engineering (MBSE) have encouraged systems engineers to transition from document-centric approaches to model-based ones. Literacy of systems engineers in reading, sharing and elaborating models has therefore become an issue. Whatever the modeling language, elaboration of models is a highly complex intellectual process and SysML is no exception. Feedback from industry practitioners and MBSE lecturers suggests that developers of SysML models often stumble on the same problem: thinking about the system before modeling it in SysML. The authors of this paper propose to ease that elaboration process by using mind maps. With their graphic form and rather flexible way of organizing ideas, mind maps turn out to be a good candidate to help thinking about the system. Unlike approaches that directly switch from mind maps to SysML diagrams dedicated to one specific system, this paper introduces an intermediate step: mind maps first enable elaboration of diagrams patterns. The latter may in turn be instantiated onto one or several systems. Without loss of generality, the proposed approach is step-wise illustrated on real-time systems monitored by software controllers. Patterns are proposed to cover need expression, requirement capture, use case driven analysis and design.

Les calculs en nombres flottants sont intensivement utilisés dans divers domaines, notamment les systèmes embarqués critiques. En général, les résultats de ces calculs sont perturbés par les erreurs d’arrondi. Dans un scenario critique, ces erreurs peuvent être accumulées et propagées, générant ainsi des dommages plus ou moins graves sur le plan humain, matériel, financier, etc. Il est donc souhaitable d’obtenir les résultats les plus précis possibles lorsque nous utilisons l’arithmétique flottante. Pour remédier à ce problème, l’outil Salsa [7] permet d’améliorer la précision des calculs en corrigeant partiellement ces erreurs d’arrondi par une transformation automatique et source à source des programmes. La principale contribution de ce travail consiste à analyser, à étudier si l’optimisation par dépliage de boucles améliore plus la précision numérique des calculs dans le programme initial. À cours terme, on souhaite définir un facteur de dépliage de boucles, c’est à dire, trouver quand est-ce qu’il est pertinent de déplier la boucle dans le programme.

Critical software based on floating-point arithmetic requires rigorous verification and validation process to improve our confidence in their reliability and their safety. Unfortunately available techniques for this task often provide overestimates of the round-off errors. We can cite Arian 5, Patriot rocket as well-known examples of disasters. These last years, several techniques have been proposed concerning the transformation of arithmetic expressions in order to improve their numerical accuracy and, in this work, we go one step further by automatically transforming larger pieces of code containing assignments, control structures and functions. We define a set of transformation rules allowing the generation, under certain conditions and in polynomial time, of larger expressions by performing limited formal computations, possibly among several iterations of a loop. These larger expressions are better suited to improve, by re-parsing, the numerical accuracy of the program results. We use abstract interpretation based static analysis techniques to over-approximate the round-off errors in programs and during the transformation of expressions. A tool has been implemented and experimental results are presented concerning classical numerical algorithms and algorithms for embedded systems.; Les systèmes critiques basés sur l’arithmétique flottante exigent un processus rigoureux de vérification et de validation pour augmenter notre confiance en leur sureté et leur fiabilité. Malheureusement, les techniques existentes fournissent souvent une surestimation d’erreurs d’arrondi. Nous citons Arian 5 et le missile Patriot comme fameux exemples de désastres causés par les erreurs de calculs. Ces dernières années, plusieurs techniques concernant la transformation d’expressions arithmétiques pour améliorer la précision numérique ont été proposées. Dans ce travail, nous allons une étape plus loin en transformant automatiquement non seulement des expressions arithmétiques mais des programmes complets contenant des affectations, des structures de contrôle et des fonctions. Nous définissons un ensemble de règles de transformation permettant la génération, sous certaines conditions et en un temps polynômial, des expressions pluslarges en appliquant des calculs formels limités, au sein de plusieurs itérations d’une boucle. Par la suite, ces larges expressions sont re-parenthésées pour trouver la meilleure expression améliorant ainsi la précision numérique des calculs de programmes. Notre approche se base sur les techniques d’analyse statique par interprétation abstraite pour sur-rapprocher les erreurs d’arrondi dans les programmes et au moment de la transformation des expressions. Cette approche est implémenté dans notre outil et des résultats expérimentaux sur des algorithmes numériques classiques et des programmes venant du monde d’embarqués sont présentés.

Les calculs en nombres flottants sont intensivement utilisés dans divers domaines, notamment les systèmes embarqués critiques. En général, les résultats de ces calculs sont perturbés par les erreurs d’arrondi. Dans un scenario critique, ces erreurs peuvent être accumulées et propagées, générant ainsi des dommages plus ou moins graves sur le plan humain, matériel, financier, etc. Il est donc souhaitable d’obtenir les résultats les plus précis possible lorsque nous utilisons l’arithmétique flottante. Pour ce faire, nous avons développé un outil qui corrige partiellement ces erreurs d’arrondi, par une transformation automatique et source à source des programmes. Notre transformation repose sur une analyse statique par interprétation abstraite qui fournit des intervalles pour les variables présentées dans les codes sources. Nous transformons non seulement des expressions arithmétiques mais aussi des morceaux de code avec des affectations, des boucles, des conditionnelles, des fonctions, etc. Les résultats obtenus par notre outils sont très prometteurs. Nous avons montré que nous améliorions de manière significative la précision numérique des calculs en minimisant l’erreur par rapport à l’arithmétique exacte des réels. Un autre critère très intéressant est que notre technique permet d’accélérer la vitesse de convergence de méthodes numériques itératives par amélioration de leur précision comme les méthodes de Newton, Jacobi, Gram-Schmidt, etc. Nous avons réussi à réduire le nombre d’itérations nécessaire pour converger de plusieurs dizaines de pourcents. Nous avons aussi étudié l’impact de l’optimisation de la précision sur le format des variables (en simple ou double précision). Pour ce faire, nous avons comparé deux programmes sources écrits en simple et en double précision avec celui transformé en simple précision. Les résultats obtenus montrent que le programme transformé (32 Bits) est très proche du résultat exact de celui de départ (64 Bits). Cela permet à l’utilisateur de dégrader la précision sans perdre beaucoup d’informations. D’un point de vue théorique, nous avons prouvé que les programmes générés n’ont pas forcément la même sémantique que les programmes d’origine, mais que mathématiquement, ils sont équivalents.

In general, the correctness of numerical computations of programs based on floating-point arithmetic is not intuitive and developers hope to compute an accurate result without guaranty. To solve this problem, we procceed by automatic source to source transformation of programs to improve their numerical accuracy.