Mémoire Online: Spécification des systèmes temps réel dans le cadre de la logique de réécriture

Mémoire online spécification et vérification des systèmes critiques (Extension de l’environnement VALID pour la prise en charge du temps réel), tutoriel & rapport PDF.

CHAPITRE 1: Introduction et Motivation
Problématique
La technologie des systèmes mixtes matériels et logiciels en anglais hardware-software (H/S) connaît de nos jours une révolution sans pareille dans tous les domaines technologiques. Le fait de mélanger matériel et logiciel, a donné naissance à des systèmes très complexes (plusieurs millions de composants électroniques et des centaines de milliers de lignes de code et même plus). La conception de tels systèmes, nécessite l’intervention de ressource humaine, financière et technologique très importante.

Aussi important soit-elle, leur modélisation, avant d’être fabriquée permet aux ingénieurs concepteurs de réduire le nombre d’erreurs de conception, connue sous l’appellation de bugs.
Pour veiller au bon fonctionnement de leurs conceptions, ces systèmes doivent être soumis à des processus de validation très rigoureux. Une telle tâche n’est point évidente vue l’accroissement rapide de la complexité et de l’hétérogénéité des nouvelles architectures H/S [Bal97]. Aussi correcte que possible, la conception doit tenir compte de certaines propriétés dites critiques, qui sans leur présence risque d’engendrer une situation de catastrophe sur le plan financier, humain et même de ternir l’image de la compagnie. En général, ces propriétés se répartissent en deux classes : propriétés de performance (durée du cycle de conception par exemple) et propriétés fonctionnelles (problèmes d’interblocage par exemple.)
La conception de composantes H/S d’un système intégré s’effectuait traditionnellement de manière séparée, c’est-à-dire que la partie logicielle obtenue, était exécutée sur le prototype de la partie matérielle. Si les contraintes de la spécification requises pour le système ne sont pas satisfaites par le design, le processus subit des modifications puis il est réitéré dans l’espoir d’obtenir le bon prototype.

Cette technique de validation s’avère être très coûteuse en temps et en coût de réalisation.
Pour parer à de telles inconvenances, plusieurs idées ont émané de la communauté scientifique pour l’élaboration de nouvelles techniques de vérification et d’environnements de co-design groupés sous l’appellation d’outils et techniques CAD (System-level Computer Aid Design) qui, en réalité, sont des plate-formes de modélisation, de validation et de synthèse, surtout de circuits VLSI (Very Large Scale Integration Circuits) [Bry91]. Comme la majeure partie des VLSI sont essentiellement des processeurs, la conception de la partie matérielle et de la partie logicielle est un problème très critique et complexe.
Aussi, compte tenu d’une compétitivité très prononcée dans un marché très ouvert tout produit conçu dans des délais moindres devient la clé du succès de tout projet.

Il est bien connu que les architectures H/S s’apparentent en général avec les systèmes enfouis (embedded), critiques et temps-réel, nécessitant qu’au moment de la phase de validation, une attention très particulière mettant en place des mécanismes de vérification tendant à éviter toute situation malencontreuse.
Au cours des dernières années, la complexité de ces systèmes (Embedded H/S Systems)[Ern98] n’a cessé de se développer. Les progrès technologiques favorables, notamment en terme de finesse de gravure, ont permis de diminuer considérablement leur taille. Cette miniaturisation entraînait incontestablement d’énormes avantages, tant au niveau de leur consommation (électronique grand public : téléphones cellulaires, distributeurs ATM…), de leur puissance et de leur rapidité.
Lors de la conception des systèmes enfouis, la phase de vérification est l’étape la plus longue.
Elle consomme jusqu’à 70 % du temps de conception. La notion de vérification elle-même, date des années soixante avec les travaux de Dijkstra et Floyd. Celle-ci, s’est étalée sur plus de trois décennies de découvertes théoriques extraordinaires qui a vu naître carrément une nouvelle science dite « vérification formelle », qui a vite déclassé certaines techniques traditionnelles telles que la simulation, le testing et les anciennes méthodes de validation. Une prise de conscience de l’importance de la vérification en tant que telle a émergée lors de la médiatisation de l’erreur de conception du Pentium d’Intel en 1994 [Pra95]. La perte a été estimée à plus de 400 millions de dollars. Ce cas n’est pas isolé, puisque de nombreux exemples d’erreurs de conception ont été médiatisées notamment le cas de l’accident lors du premier vol du lanceur européen ARIANE-5[Ari96, RSS96] en 1996 (Figure 1.1) qui a été suivi de la vérification du système complet par des techniques d’interprétation abstraite, ce qui a permis la suppression de certaines erreurs parmi elles, celles ayant entraîné la destruction de la fusée.
………..

Si le lien ne fonctionne pas correctement, veuillez nous contacter (mentionner le lien dans votre message)
Spécification et vérification des systèmes critiques (Extension de l’environnement VALID pour la prise en charge du temps réel) (1,25 Mo) (Rapport PDF)
Vérification des systèmes critiques

Télécharger aussi :

Laisser un commentaire

Votre adresse e-mail ne sera pas publiée. Les champs obligatoires sont indiqués avec *