Le résumé dans les écrits académiques

Plusieurs organisations environnementales à but non lucratif tentent de s’opposer aux conséquences négatives du changement climatique. Afin de financer leurs activités, elles réclament des donations. Pourtant, à l’heure actuelle, le nombre de personnes faisant des dons aux organisations environnementales ne cesse de décroître, ce qui provoque un écart de financement. Si ces organisations souhaitent poursuivre leur travail, le nombre de dons doit augmenter.

L’objectif de cette étude est d’évaluer la possibilité d’augmenter les intentions de don des individus à une organisation environnementale. La problématique est par conséquent la suivante : dans quelle mesure la distance sociale entre un donneur potentiel et les victimes du changement climatique présentées dans les campagnes de levées de fonds peuvent affecter son intention de don ? Dans ce contexte, la distance sociale correspond à l’impression ressentie par les individus d’appartenir au même groupe social ou à un groupe social différent, en lien avec les victimes des changements climatiques.

Pour répondre à la problématique, une expérience incluant la distribution d’un questionnaire en ligne a été conduite. Les participants ont été répartis de façon aléatoire en deux groupes (à savoir distance sociale réduite ou étendue). À partir de cette classification, il leur a été demandé de commenter une image issue d’une campagne de levée de fonds. Les réponses récoltées montrent que le ressenti d’une distance sociale étendue augmente les intentions de don des individus. Ces résultats indiquent que la distance sociale joue réellement un rôle sur les intentions de don.

À partir de ces conclusions, les groupes environnementaux peuvent s’attacher à représenter une distance sociale conséquente lors des campagnes de levée de fonds dans le cadre de leurs activités liées aux changements climatiques. Des recherches ultérieures devraient permettre d’identifier d’autres facteurs utiles à ce type d’organisations lorsqu’elles sélectionnent les images les mieux adaptées à ce type de campagne.

Les systèmes embarqués sont de plus en plus intégrés dans les applications temps réel actuelles. Ils sont généralement constitués de composants matériels et logiciels profondément intégrés, mais hétérogènes. Ces composants sont développés sous des contraintes très strictes. En conséquence, le travail des ingénieurs de conception est devenu plus difficile.

Pour répondre aux normes de haute qualité dans les systèmes embarqués de nos jours et pour satisfaire aux besoins quotidiens de l’industrie, l’automatisation du processus de développement de ces systèmes prend de plus en plus d’ampleur. Un défi majeur est de développer une approche automatisée qui peut être utilisée pour la vérification intégrée et la validation de systèmes complexes et hétérogènes.

Dans le cadre de cette thèse, nous proposons une nouvelle approche compositionnelle pour la modélisation et la vérification des systèmes complexes décrits en langage SystemC. Cette approche est basée sur le modèle des SystemC Waiting State Automata (WSA). Les SystemC Waiting State Automata sont des automates permettant de modéliser le comportement abstrait des systèmes matériels et logiciels décrits en SystemC tout en préservant la sémantique de l’ordonnanceur SystemC au niveau des cycles temporels et au niveau des delta-cycles. Ce modèle permet de réduire la complexité de la modélisation des systèmes complexes due au problème de l’explosion combinatoire tout en restant fidèle au système initial. Ce modèle est compositionnel et supporte le raffinement. De plus, il est étendu par des paramètres temps ainsi que des compteurs afin de prendre en compte les aspects relatifs à la temporalité et aux propriétés fonctionnelles comme notamment la qualité de service. Dans le cadre de cette thèse, nous proposons une chaîne de construction automatique des WSAs à partir de la description SystemC. Cette construction repose sur l’exécution symbolique et l’abstraction des prédicats.

Nous proposons un ensemble d’algorithmes de composition et de réduction de ces automates afin de pouvoir étudier, analyser et vérifier les comportements concurrents des systèmes décrits ainsi que les échanges de données entre les différents composants. Nous proposons enfin d’appliquer notre approche dans le cadre de la modélisation et la simulation des systèmes complexes. Ensuite, l’expérimenter pour donner une estimation du pire temps d’exécution (worst-case execution time (WCET)) en utilisant le modèle du Timed SystemC WSA. Enfin, on définit l’application des techniques du model checking pour prouver la correction de l’analyse abstraite de notre approche.

Mots clés : SystemC, Méthodes Formelles, Automates, Exécution Symbolique, Abstraction des prédicats, Sémantiques des langages, Model Checking.