Soutenance mémoire
Dans la société moderne, les technologies embarquées sont devenues importantes, voire indispensables. En effet, elles sont de plus en plus implantées dans divers domaines de la vie courante : personnel, transport, assistance et domaine médical. Les progrès technologiques permettent de concevoir des systèmes de plus en plus complexes avec des contraintes fonctionnelles et non fonctionnelles de plus en plus exigeantes.
La complexité de ces systèmes a explosé à cause de l’intégration de grand nombre de composants sur une même surface, dits “systèmes sur puce”. L’accroissement de cette complexité conjugué aux exigences de qualité, de performance et économique demandent que soient repensées les méthodes permettant de concevoir et de valider ces systèmes. Les méthodologies et outils de conception doivent permettre de construire des systèmes de fonctionnalité déterminée, de qualité et garantie, à coût acceptable. Pour répondre à cette problématique de nouvelles approches de conception ont vu le jour, ces approches se basent sur :
• L’identification des décisions de conception tôt dans le flot de conception. Les modifications tardives de conception sont coûteuses en temps, ainsi estimer les performances du système tôt permet de réduire les coûts de conception et d’accroître la productivité.
• La modélisation à des niveaux abstraits visant des simulations rapides et des vérifications en amont sur des modèles simples, raffinés ensuite jusqu’au niveau des portes logiques et/ou la génération d’un code exécutable.
• L’exploration d’architecture par une séparation entre la description du fonctionnement d’un système (dite application) et l’architecture matérielle sur laquelle le système va s’exécuter après une étape de liaison (dite de projection). Cette séparation permet la validation du fonctionnement indépendamment de l’architecture et la réutilisation de la même application sur plusieurs architectures.
• L’introduction des méthodes formelles dans le processus de développement des systèmes sur puce. Le développement de systèmes critiques requiert la vérification exhaustive de leurs fonctionnements. Les techniques de vérification par ”model checking” qui sont basées sur l’exploration d’états du système sont devenues un classique pour des vérifications en aval dans le processus de développement d’un système. L’avantage de ces techniques est la possibilité d’automatisation du processus de preuve et aussi la possibilité de générer un contre exemple dans le cas de violation de la propriété vérifiée.
• La réutilisation du code existant et des modèles développés dans des projets précédents. La réutilisation des composants préalablement conçus dans un autre contexte peut entraîner une réduction considérable dans le temps et le coût de conception. Généralement, les nouveaux produits sont une évolution des produits existants et rarement une révolution.
La vérification formelle est la phase la plus coûteuse dans la conception des systèmes, cette phase se heurte au problème de la taille des systèmes et au temps nécessaire pour sa réalisation. La conception des systèmes par des niveaux d’abstraction permet de gérer la complexité de ces systèmes et donc réduire le temps nécessaire pour la vérification. Toutefois, le processus d’ajout des détails et le passage entre les différents niveaux de description du système est réalisé par le concepteur, ce qui crée une source potentielle d’introduction d’erreurs de fonctionnement et impose la vérification à posteriori des propriétés. Ainsi, la vérification devient rapidement très coûteuse sur les niveaux les plus bas. Par conséquent, la majorité des circuits sur le marché sont validés presque exclusivement par des tests fonctionnels et ne sont pas vérifiés à 100%, ils peuvent donc renfermer des bugs. Dans nos travaux, nous nous sommes intéressés à l’amélioration de la phase de vérification formelle dans les approches de conception par niveaux.
Conception des systèmes embarqués
Informellement, on peut définir les systèmes embarqués comme étant des composants électroniques issus d’une combinaison de composants logiciels et composants matériels qui interagissent continuellement avec leur environnement. Les composants logiciels sont utilisés pour leur flexibilité tandis que les composants matériels sont utilisés pour l’augmentation des performances et la réduction de la consommation d’énergie. Ces systèmes jouent un rôle important dans de nombreux domaines d’application de plus en plus critiques tels que le domaine de la santé, la conduite assistée, la communication et d’autres domaines dans lesquels leur dysfonctionnement peut générer des pertes économiques ou des conséquences inacceptables pouvant aller jusqu’à des pertes en vies humaines. La conception de tels systèmes doit offrir des garanties de bon fonctionnement et de robustesse en cas de défaillance d’une partie de celui-ci ou lors de la survenue d’un événement non prévu.
De nos jours, de nouvelles approches et environnements de conception se sont développés pour répondre à la complexité croissante des systèmes embarqués, notamment les systèmes sur puce. Pour gérer cette complexité, ces approches se basent sur la description du système à différents niveaux d’abstraction. Ces approches doivent alors : (1) décrire une démarche claire allant du modèle abstrait jusqu’à la génération du code ; (2) faciliter au concepteur la modélisation, l’analyse, la vérification, l’exploration, le raffinement, et la synthèse et (3) permettre la réutilisation et la modification des composants lors de processus de conception. Dans cette section, nous allons tout d’abord montrer les différents niveaux et vues d’un système, puis définir un flot de conception d’un système embarqué ; nous nous basons sur les flots de conception qui commence par le niveau système. Ensuite, nous allons voir les différents environnements de conception, leurs approches et à quoi ils répondent. Enfin, nous dégageons la problématique de cette thèse.
Niveaux et vues d’un système
Il existe plusieurs niveaux de description d’un système embarqué. Les deux niveaux les plus utilisés sont le niveau RTL (Register Transfer Level) et le niveau système. Dans le niveau niveau RTL le système est représenté en terme de transfert de données entre les registres, des signaux de contrôles, et d’opérations logiques sur les signaux de contrôle et de données dans des composants de calcul. Dans ce niveau, l’échantillonnage des valeurs des signaux et les transferts sont cadencés par une horloge. C’est à ce niveau que sont construits les composants matériels tels que, les bus, les propriétés intellectuelles (IPs), les interfaces et d’autres composants. Le niveau RTL peut être utilisé pour une description exclusivement matérielle d’un système, mais il ne permet pas la description du fonctionnement implémenté en logiciel. Aussi, ce niveau est très détaillé ce qui rend l’analyse et la simulation très lentes. Pour répondre à ce problème de complexité et d’hétérogénéité, le système est représenté dans un niveau plus abstrait dit niveau système. Dans ce niveau, une représentation d’un système décrit le parallélisme entre les différents processus s’exécutant en matériel et en logiciel ainsi qu’une échelle de temps macroscopique indiquant les temps de calcul et de transfert de données.
En addition aux différents niveaux de description d’un système embarqué, celui-ci peut être modélisé selon trois vues quel que soit le niveau de description choisi. Ces vues correspondent à trois caractéristiques différentes et complémentaires du même système [48, 49] : fonctionnelle, structurelle et physique. La vue fonctionnelle représente le comportement d’un système avec les échanges des données d’entrées/sorties dans le temps sans donner des détails sur la structure et la géométrie de celui-ci. Dans cette vue, le parallélisme d’un système n’implique pas forcément une concurrence lors de son implémentation sur une plate-forme réelle. Le fonctionnement d’un système est décrit dans un langage spécifique selon le besoin de spécification et le niveau d’abstraction choisi. Par exemple, dans le niveau système le fonctionnement est décrit par des langages de flot de données comme les réseaux de KAHN [71] ou un langage de programmation comme le langage C ou SYSTEMC[89, 9] et SPECC[47] ; Par contre, dans le niveau RTL le fonctionnement d’un système est écrit dans les langages de description matériel HDL comme VHDL et VERILOG. La vue structurelle d’un système représente la structure des composants et leurs interconnexions en faisant abstraction des détails de calcul et de communication. Dans le niveau système, la structure est décrite par une interconnexion de composants de calcul, de communication, de stockage et d’interfaçage ; Dans le niveau RTL la structure est composée par des blocs de registres, des unités de calcul (UAL) et des bus. Dans la vue physique d’un système, on rajoute l’information de dimension à la structure du système ce qui permet de donner les informations concernant la taille de chaque composant, sa position et aussi la position de chaque porte dans le système. Cette vue est représentée par des paramètres physiques de la structure des composants. Ces paramètres du système sont liés aux technologies de construction des transistors et sont peu (ou pas) exploitables sur le niveau système.
Il existe plusieurs approches de conception, dites aussi flots de conception, de systèmes embarqués, qui sont basés sur différents niveaux et vues d’un système. Ces approches peuvent être classées selon : les niveaux et les vues utilisés, les relations entre les différents niveaux d’abstraction et entre les vues, le type de plate-forme visée (fixe ou dynamique) et aussi le type de langage de modélisation utilisé. Un des flots pour la conception des systèmes consiste à développer et à étudier chaque composant indépendamment des autres dans un niveau détaillé avant de les assembler pour la construction d’un système global. Cette approche ne permet pas d’avoir une vue globale sur le système avant la construction de ces composants, ce qui cause la détection tardive des erreurs à la construction du système. Pour répondre à ce problème, les environnements actuels de développement des systèmes embarqués, se basent sur le flot de conception système [48]. Ce flot de conception permet la description d’un système dans sa globalité dans le niveau système et permet ainsi le développement conjoint des composants logiciels/matériels. Il permet la modélisation d’un système à différents niveaux d’abstraction allant du niveau système vers le niveau RTL. Dans la suite de ce chapitre, nous nous intéressons à ce flot de conception système, nous parcourons les différents travaux de recherche visant l’amélioration de ce flot, les différents problèmes rencontrés et nous finissons par la proposition d’une piste de solutions possibles.
|
Table des matières
INTRODUCTION
I Contexte et État de l’art
1 Problématique et état de l’art
1.1 Conception des systèmes embarqués
1.1.1 Niveaux et vues d’un système
1.1.2 Flot de conception système
1.1.3 Environnements de conception
1.1.4 Problématique
1.2 Vérification des systèmes embarqués
1.2.1 Validation par simulation
1.2.2 Vérification par “Model-Checking”
1.2.3 Vérification par “Theorem-Proving”
1.2.4 Raffinement formel
1.2.5 Raffinement formel dans les systèmes embarqués
1.3 Notre proposition
1.3.1 Cadre méthodologique
1.3.2 Niveau abstrait de modélisation
1.3.3 Raffinement de communication guidé
1.3.4 Contributions
1.4 Conclusion
II Contributions
2 Cadre méthodologique
2.1 Méthodologie en Y
2.1.1 Modèle d’application
2.1.2 Modèle d’architecture
2.1.3 Famille de bus
2.1.4 Projection/ Partitionnement
2.2 Raffinement de communication
2.2.1 Premier raffinement : Changement de granularité de données
2.2.2 Second raffinement : Gestion des canaux
2.2.3 Troisième raffinement : Introduction de bus abstrait
2.2.4 Résumé des étapes de raffinement
2.3 Conclusion
3 Formalisme
3.1 Pomset
3.1.1 Algèbre de Pomset
3.1.2 Extension sur l’algèbre des pomsets
3.2 Sémantique TML
3.2.1 Sémantique d’une tâche
3.2.2 Sémantique d’un canal
3.3 Les systèmes de transitions finis
3.3.1 Sémantiques de raffinement des systèmes de transition
3.3.2 Traduction des pomsets aux LTSs
3.4 Conclusion
4 Raffinement des canaux de communication
4.1 Premier raffinement : Changement de granularité de données
4.1.1 Transformation du modèle des canaux
4.1.2 Transformation des modèles des tâches
4.2 Second raffinement : Gestion des canaux
4.2.1 Transformation du modèle des canaux
4.2.2 Transformation du modèle des tâches
4.3 Troisième raffinement : Introduction de bus abstrait
4.3.1 Arbitre
4.3.2 Interfaces de communication
4.3.3 Transformation du modèle des tâches
4.4 Schéma de notre démarche de raffinement et de vérification des niveaux 1, 2 et3
4.4.1 Application des transformations
4.4.2 Génération des modèles LTS
4.4.3 Étude de raffinement
4.5 Conclusion
III Étude de cas et conclusion
5 Étude de cas
5.1 Exemple d’application : Appareil photo numérique
5.1.1 Les principaux modules de l’application
5.1.2 Description TML de l’application
5.1.3 Architecture et partitionnement
5.1.4 Analyse de propriétés
5.2 Démarche de raffinement des canaux de communication
5.2.1 Premier raffinement : Changement de granularité de données
5.2.2 Second raffinement : Gestion des canaux
5.2.3 Troisième raffinement : Introduction de bus abstrait
5.3 Analyse de préservation de propriétés
5.3.1 Première stratégie de validation
5.3.2 Seconde stratégie de validation
5.4 Conclusion
CONCLUSION
Bibliographie
Télécharger le rapport complet
