L'introduction du temps dans les bases de données classiques et spatiales apparaît de plus en plus, aujourd'hui, comme une nécessité pour une gestion optimale de l'historicité. En effet, les applications de bases de données spatio-temporelles sont présentes dans un grand nombre d'applications. Le besoin, par exemple, est de sauvegarder l'historique des géométries des parcelles dans le système d'information d'un plan cadastral, la prévention d'incendie dans le système de gestion forestière, le système de navigation des véhicules, etc. Cet historique des phénomènes permet de mieux comprendre ce qui s'est produit dans le passé, de manière à éventuellement anticiper certaines évolutions futures. Etant donné ces nouveaux besoins, cette thèse se focalise sur la modélisation et l'implantation des aspects temporels dans bases de données. En effet, la conception d'une application de base de données se fait par un enchaînement de trois phases (conceptuelle, logique et physique). Au niveau conceptuel, plusieurs modèles conceptuels ont été proposés intégrant les caractéristiques temporelles et spatiales. Malheureusement, au niveau logique, les modèles de données des SGBD actuels n'offrent pas les concepts nécessaires pour implanter le modèle conceptuel spatio-temporel. Nous proposons donc de nouvelles règles de traductions d'un schéma conceptuel, basé sur le modèle MADS (Modélisation des Applications à des données spatio-temporelles), en un schéma logique MADSLog pour les modèles cibles à savoir : relationnel et relationnel-objet. Chaque règle transforme un concept structurel, temporel et spatial du modèle MADS en un ou plusieurs concepts supportés par la cible. Par exemple, la propriété spatiale définissant la géométrie d'un type d'objet est traduite par la création d'un nouvel attribut de type spatial dans ce type d'objet. Un outil CASE(Computer-Aided Software Engineering) appelé Schema Translateur est développé dans cette thèse implémentant toutes les règles de traductions. La traduction de schémas conceptuels en schémas logiques peut impliquer une perte sémantique en raison de la différence de la puissance d'expression entre le modèle conceptuel et le modèle de données des SGBD existants. D'où la nécessité de générer un ensemble de contraintes d'intégrité afin de préserver la sémantique définie dans le schéma conceptuel. Ces contraintes sont exprimées à ce niveau par des formules logiques. Avec l'apparition de GML (Geographic Markup Language ) qui est conçu pour la modélisation, le transport et le stockage d'informations géographiques. Nous transformons également le schéma conceptuel MADS en GML. De nouveaux schémas GML temporel et spatial sont définis qui peuvent être employés par n'importe application de base de données spatio-temporelle. Au niveau physique, nous proposons une méthode d'adaptation du schéma logique en schéma physique pour le modèle relationnel-objet. Elle permet de définir les tables, les types abstraits, les types d'objets, les domaines, etc. Notre proposition permet aussi la génération des contraintes d'intégrité au niveau physique. En effet, chaque contrainte d'intégrité (structurelle, temporelle ou spatiale) qui est définie en calcul logique est exprimée soit directement par des contraintes déclaratives ou soit par des déclencheurs du SGBD choisi. Les déclencheurs spatiaux sont fondés sur les fonctionnalités prédéfinies dans Oracle, alors que les déclencheurs temporels sont basés sur les opérateurs et méthodes appliquées sur les types temporels. Enfin, la traduction de requêtes est une deuxième clef de cette recherche. Le but de la traduction de requêtes, exprimées en algèbre, étant de reconstituer l'information au sens MADS à partir de la base de données stockées dans le SGDB cible. Elle permet de traduire les expressions algébriques MADS, qui sont définies sur le schéma conceptuel et non sur le schéma physique, en requêtes opérationnelles qui peuvent être exécutées sur une base de données spatiale et temporelle sous un SGBD ou un SIG.

Thèse (Ph.D.)--Université Laval, 2009. / Bibliogr.: f. 111-120. Publié aussi en version électronique dans la Collection Mémoires et thèses électroniques.

Résumé : Les résultats d'une étude expérimentale sur les possibilités d'utilisation des systèmes radar dans l'évolution temporelle de l'humidité du sol sont présentés. Une campagne de terrain a été conduite durant tout un cycle de croissance sur un couvert de blé. Les mesures ont été obtenues à l'aide d'un diffusomètre radar à 5.17 GHz, en polarisation HH, pour six angles d'incidence. Les données incluent deux directions d'illumination, l'une parallèle à l'orientation des rangs (13=0°) et l'autre perpendiculaire (13=90°). Des analyses de régression et une analyse graphique de l'évolution temporelle de a° ont démontré que la conversion des données radar en valeur d'humidité du sol devient difficile lorsque le taux d'humidité se situe en deça d'un certain seuil (-20%). Il a été démontré également que les changements dans la morphologie de la plante peuvent causer des variations extrêmes des valeurs de rétrodiffusion et présenter de ce fait une ambiguïté dans l'interprétation de l'humidité du sol. ||Abstract : The results of experimental studies on the use of radar to mesure the temporal evolution of soil moisture are presented. An experiment was conducted using the FM microwave scatterometer of the Canada Centre for Remote Sensing. The radar measurements were made during all growing season at 5.17 GHz, HH polarization, and at six incidence angles. Two row aspects of the wheat fields were included, one parallel to the furrows (13=0°) and the other perpendicular (13=90°). Regression analysis followed by graphic analysis of the temporal evolution of a° show that for a certain range of soil moisture the temporal evolution is ambiguous. This occurs when soil moisture is relatively low, resulting in saturation of the radar backscatter. A positive inversion of the curve is observed when soil humidity is lower than a certain threshold 20%). Moreover it is shown that temporal plant morphology variations can cause extreme variations in the values of the scattering coefficient

Nous etendons les logiques temporelles du temps alternant ATL et ATL* au moyen de contextes strategiques et de contraintes sur la memoire : la premiere extension permet aux agents de s'en tenir a leurs strategies lors de l'evaluation des formules, contrairement a ATL ou chaque quantificateur de strategies ecrase les strategies anterieurement selectionnees. La seconde extension permet aux quantificateurs de strategies de se restreindre aux strategies sans memoire ou avec memoire bornee. Nous avons l'etudie l'expressivite de nos logiques. Nous montrons qu'elles expriment des proprietes importantes comme l'exstence d'equilibres, et nous les comparons formellement a d'autres formalismes proches (ATL, ATL*, Game Logic, Strategy Logic, ...). Nous avons aborde les problemes de model-checking. Nous donnons un algorithme PSPACE pour la logique n'impliquant que des strategies sans memoire, et un algorithme EXPSPACE pour le cas des strategies a memoire bornee. Dans le cas general, malgre leur forte expresssivite, nous prouvons que leur model-checking reste decidable par un algorithme a base d'automates d'arbres alternants qui permet d'evaluer une formule sur la classe complete des CGS avec n joueurs. / We extend the alternating-time temporal logics ATL and ATL* with strategy contexts and memory constraints: the first extension make agents commit to their strategies during the evaluation of formulas, contrary to plain ATL where strategy quantifiers reset previously selected strategies. The second extension allows strategy quantifiers to restrict to memoryless or bounded-memory strategies. We consider expressiveness issues. We show that our logics can express important properties such as equilibria, and we formally compare them with other similar formalisms (ATL, ATL*, Game Logic, Strategy Logic, ...). We address the problem of model-checking for our logics, especially we provide a PSPACE algorithm for the sublogics involving only memoryless strategies and an EXPSPACE algorithm for the bounded-memory case. In the general case, despite the high expressiveness of these logics, we prove that their model-checking problems remain decidable by designing a tree-automata-based algorithm for model-checking ATLsc on the full class of n-player concurrent game structures.

Mémoire numérisé par la Direction des bibliothèques de l'Université de Montréal.

Thèse numérisée par la Direction des bibliothèques de l'Université de Montréal.

Les travaux de cette thèse ont pour cadre l'édition de documents électroniques multimédia en considérant en tout premier lieu leur dimension temporelle (enchaînement des objets dans le temps). L'objectif concerne à la fois l'intégration de cette nouvelle dimension dans la structure globale d'un document (logique, spatiale et hypertexte) et l'intégration d'objets de base qui ont eux-mêmes une dimension temporelle (vidéo, audio, interactions de l'utilisateur ..). Les documents visés sont donc multimédia, temporisés et interactifs. Notre étude a porté tout d'abord sur la définition d'un langage temporel multimédia. Celui-ci permet de spécifier, de façon déclarative, le scénario temporel d'un document en s'appuyant sur des résultats obtenus dans le domaine de la satisfaction de contraintes temporelles et de la planification. Nous avons ensuite conçu des mécanismes d'analyse qui permettent la vérification de la cohérence d'une spécification tout en prenant en compte trois aspects essentiels aux systèmes multimédia : l'incrémentalité, l'efficacité, et la gestion de l'indéterminisme. Nous proposons des mécanismes de synthèse qui permettent alors le calcul d'une solution qui sera exploitée par le système de présentation. Celui-ci permet, à partir d'un automate d'états finis extrait du graphe temporel de contraintes, d'exécuter la présentation multimédia et de contrôler dynamiquement son déroulement. Enfin, nous présentons l'ensemble des résultats à travers leur application concrète au sein d'un outil d'édition et de présentation appelé Madeus.

Cette thèse propose un nouveau type de systèmes de ré-écriture, appelé les systèmes de réécriture fonctionnels. Nous montrons que notre modèle a la puissance d'expression des systèmes de ré-écriture et qu'il est bien adapté à l'étude de propriétés de sûreté et de propriétés de logique temporelle de modèles.Nous avons mis en évidence une sous classe de systèmes fonctionnels, les élémentaires et les élémentaires à droite, préservant la puissance d'expression des systèmes fonctionnels et des techniques d'accélération des calculs aboutissant à un outil de vérification symbolique efficace.Dans la partie expérimentale, nous avons comparé notre outil, d'une part avec des outils de ré-écriture tels que Timbuk, Maude et TOM, d'autre part avec des outils de vérification tels que SPIN, NuSMV, SMART, HSDD. Nos benchmarks démontrent l'efficacité des systèmes fonctionnels élémentaires pour la vérification de modèles.

L’objectif du project FerroCOTS est de faire évoluer l’architecture de contrôle-commande ferroviaire embarqué des relais électriques vers des Composant-sur-Etagère (COTS) programmables, ici des cartes FPGA (Field-Programmable Gate Array en anglais). Toutefois, l'absence d’une méthode appropriée de spécification et vérification formelles est un obstacle important au développement d’une architecture de contrôle-commande à base de COTS. Dans cette thèse, nous proposons tout d'abord des techniques systématiques de raffinement des exigences brutes et qui permettent de transformer des exigences informelles en des spécifications formelles, tout en guidant et assistant le processus de raffinement et l'étape de formalisation. En l'occurrence, deux méthodes de raffinement des exigences ont été développées. Le cadre de formalisation choisi pour cette méthode de formalisation des exigences est la logique temporelle CTL*, qui est un sur-ensemble des logiques CTL (Computation Tree Logic en anglais) et LTL (Linear Time Logic en anglais). Ainsi, les exigences raffinées peuvent être formalisées à l'aide de CTL*. En outre, ces formules en CTL* offrent une base formelle pour la vérification et la validation du système. Puis, à partir des spécifications formelles exprimées sous forme de propriétés CTL*, nous présentons une méthode pour générer des scénarios de test à partir des formules CTL*. La méthode de test utilise le concept de « non-vacuité » pour générer des scénarios de test « Intelligents », qui soient capables de conduire la simulation à une réfutation d’une propriété pour que les bugs dans un système sous test peuvent être détectés. / The goal of the FerroCOTS project is to develop an architecture of embedded railway command/control systems from electrical relays towards programmable Commercial-Off-The-Shelf (COTS) components, here some high-speed Field-Programmable Gate Array (FPGA) digital devices. However, the lack of appropriate formal specification and verification means is a huge obstacle to develop a COTS based control/command architecture. In this thesis, firstly we propose systematic requirement refinement techniques to transform informal requirements into formal specifications, while guiding and assisting the refinement process and the formalization step. In this case, two requirement refinement methods have been developed. The formalization framework chosen for requirement formalization is the temporal logic CTL*, which is a superset of the logic Computation Tree Logic (CTL) and the Linear Time Logic (LTL). Thus, the refined requirements are formalized using CTL*. In addition, the obtained CTL* formulas provide a formal basis for system verification and validation. On the other hand, based on formal specifications expressed as CTL* properties, we present a method for generating test cases from CTL* formulas. The test method uses the concept of non-vacuity to generate “Intelligent” test benches that are capable of driving the simulation to a property refutation so that the bug of the system under test can be detected.

Notre travail de recherche est consacré à l'analyse, d'un point de vue aspectuel, du rôle de la morphologie dérivationnelle dans le processus de construction du sens aspectuel lexical. Le préfixe RE- est très intéressant parce que sa structure processuelle est complexe. Il implique une relation entre un procès présupposé et un procès posé et cette relation est établie par un troisième procès, intermédiaire, qui crée un lien de continuité, de reprise ou d'interruption. L'activation de ces liens est notamment dépendante du sens de la base lexicale du dérivé et du sens aspectuel de cette même base. Le préfixe RE- est donc un opérateur de dérivation dont une des valeurs est aspectuo-temporelle et agit sur deux dimensions de la temporalité linguistique : la première est quantitative, il s'agit de l'itération ; la seconde est qualitative, elle traduit la relation temporelle établie entre les trois procès signifiés par le dérivé. / Our research is centered on the analysis of the role of morphological derivation in the elaboration of the lexical aspectual meaning. The prefix RE- is particularly interesting because of the complexity of its processual structure. RE- implies a relation between a presupposed process and a posited process, and this relation is established by a third - intermediate - process, which can signify continuity, resumption or interruption. The activation of this relation depends in particular on the meaning of the lexical base of the derived term and on the aspectual meaning of this base. The prefix RE- is thus an operator of derivation which possesses a temporal/aspectual value acting on two dimensions of linguistic temporality : the first, iteration, is quantitative, and the second is qualitative, as it expresses the temporal relation established between the three processes signified by the derived term.