This thesis project will explore the landscape site development of fossil fuel steam electric stations as it is presently practiced by electric utility companies, to determine what architectural, engineering, aesthetic, and climatological problems are being created through the engineering requirements acting upon' the site during site development and construction phases of power stations. It will identify typical problem areas that can be resolved by the Landscape Architect through the practical application of landscape architecture principles, the design use and influence of plant material, topography, and the environment. Design criteria will then be formulated for the site development of steam electric stations. The design criteria thus gathered will be applied to a critique of Huntington Canyon Electric Power Plant to determine the effectiveness and degree of success of the criteria.

Embedded real-time applications have to allow interaction between the control computer and the controlled environment. Controlling the environment requires in particular to take into account its time constraints and critical logical conditions. One of the main programmer efforts in real-time application's development is to trace the incoming events, and to perform reactions based on the current system status, according to the application requirements. All this have to be handled, although external events may come in the middle of a critical reaction, which may disturb it. This problem involves two difficulties: „X The cognitive efforts to percept the problem, and consequently to express the solution. „X The correct translation of this solution to code. Two requirements were defined in this research in order to achieve high-quality performance: clearness and robustness, clearness in the design, and robustness in the execution. In this work the author proposes a methodology and a tool for real-time application's development that uses or implies an innovated form of design based on natural-cognitive researches. This design method has clear compilation's rules to produce an Object-Oriented light-code, suitable for embedded platforms. These compilation's rules introduce to the code implicit security and synchronization's elements, to support robust execution. In this methodology, clear development phases were defined, using a high-degree of reuse and even polymorphism, which were emphasized in the research. Several existing ideas were improved/adapted and synthesized together with the author's innovation, creating the Arts'Codes method for real-time application development. The work includes cognitive evaluations, assuring the natural skills of the design. Arts'Codes method proposes a natural VPL (Visual Programming Language) for real-time applications, based on hierarchic components. This VPL is built on a minimum of diagrams: one for the static architecture and one for the dynamic behaviour, with a similar restricted notation at all levels. These two diagrams (static architecture and dynamic behaviour) are interleaved in a unified view. This method was implemented by building a suitable graphic editor, which automatically compiles the applications diagrams in a light and robust Object-Oriented code (based on Parallel Automata FSM), and by building an execution compact software platform. Furthermore, the parallel automata FSM are translated automatically in PTL temporal formula defining the goals and the behaviours of the components, permitting to prove a-priory that the components behaviours are consistent to their goals. The execution platform is based on a restricted implementation of the synchrony hypothesis and on a powerful model of execution: the parallel automata FSM. These Parallel Automata describe the dynamic behaviours of the components and allows implementing run-time exceptions handling too. In addition, the research proposes a tri-processor execution hardware platform, which supports a hybrid synchronous/multi-threading execution. This method will contribute to versatile, clear and robust real-time application's development.

La préservation de propriétés établies sur le programme source jusqu'au code exécutable est un point important dans les méthodes formelles. Cette propriété de préservation est établie par la vérification formelle du proccessus de compilation. Un compilateur est formellement vérifié s'il est accompagné d'une preuve de préservation sémantique : "si la compilation réussit, le code compilé se comporte comme le code source le prédit." Le projet CompCert étudie la vérification formelle de compilateurs réalistes utilisable dans l'embarqué-critique. Il s'agit de développer et formellement vérifier de tels compilateur via l'assistant de preuve Coq. Un compilateur pour le langage C vers l'assembleur PowerPC a déjà ainsi été produit. Le code exécutable du compilateur a été obtenu en deux étapes non vérifiés : la génération automatique de code Ocaml par le mécanisme d'extration de Coq et la compilation du de ce code extrait par le système Objective Caml. En fait, cette lacune est commune à tous les développements spécifiés dans l'assistant de preuve Coq et destinés à produire un éxécutable. Cette thèse décrit l'étude, le développement et la vérification formelle, dans l'assistant de preuve Coq, d'un compilateur pour le fragment purement fonctionnel du langage ML : le langage cible du mécanisme d'extraction de Coq. Concrètement, il s'git d'une chaîne de compilation en amont pour mini-ML (lambda calcul, let, letrec et filtrage) vers le premier langage intermédiaire de la chaîne de compilation en aval du compilateur CompCert. Ce langage, Cminor, est un langage de bas niveau à la C. L'expressivité du langage source traité rend ce compilateur réaliste. Il comporte aussi des optimisations classiques propre à la compilation de langages fonctionnels : la décurryfication, comme celle implémentée dans le compilateur OCaml ; la représentation uniforme des données, explicitation des fermetures, numérotation des constructeurs et une mise en style par passage de continuation (CPS) optimisée. Le point fort de ce compilateur et que, comme les compilateurs modernes pour langage de haut niveau, il peut interagir avec un gestionnaire de mémoire automatique. Cette interaction a aussi été formellement vérifiée.

LOTOS (Language Of Temporal Ordering Specification) est un langage <br />de description de systemes paralleles communicants, normalise par l'ISO et le <br />CCITT afin de permettre la definition formelle des protocoles et des services<br />de telecommunications. Le langage utilise des types abstraits algebriques pour<br />specifier les donnees et un calcul de processus proche de CSP et CCS pour<br />exprimer le controle. <br /><br /> Cette these propose une technique de compilation permettant de traduire <br />un sous-ensemble significatif de LOTOS vers un modele reseau de Petri<br />interprete (pouvant servir a produire du code executable) puis vers un<br />modele automate d'etats finis (permettant la verification formelle de programmes<br />LOTOS soit par reduction ou comparaison modulo des relations d'equivalence, soit<br />par evaluation de formules de logiques temporelles).<br /><br /> La methode employee differe des approches usuelles basees sur la<br />reecriture de termes, qui construisent directement le graphe d'etats<br />correspondant a un programme LOTOS. <br /> Ici au contraire la traduction est effectuee en trois etapes successives<br />(expansion, generation et simulation) s'appuyant sur des modeles semantiques<br />intermediaires (le langage SUBLOTOS et le modele reseau). Elle met en oeuvre<br />une analyse statique globale du comportement des programmes.<br /> Elle prend en compte les donnees, celles-ci devant etre compilees<br />au moyen dalgorithmes deja existants.<br /><br /> Ces principes de compilation ont ete entierement implementes dans<br />le logiciel CAESAR. Les performances obtenues confirment l'interet de la methode.

L'objectif principal de cette thèse est l'étude et la formalisation de nouvelles constructions permettant d'augmenter l'expressivité du filtrage et des langages à base de règles en général. Ceci est motivé par le développement de Tom, un système qui enrichit les langages impératifs comme Java et C avec des constructions de haut niveau comme le filtrage et les stratégies. Une première extension que l'on propose est la notion d'anti-patterns, i.e. des motifs qui peuvent contenir des symboles de complément. La négation est intrinsèque au raisonnement habituel, et la plupart du temps quand on cherche quelque chose, on base nos motifs sur des conditions positives et négatives. Cela doit naturellement se retrouver dans les logiciels permettant les recherches à base de motifs. Par exemple, les anti-patterns permettent de spécifier qu'on cherche des voitures blanches qui ne sont pas des monospaces, ou qu'on cherche une liste d'objets qui ne contient pas deux éléments identiques. Nous définissons alors de manière formelle la sémantique des anti-patterns dans le cas syntaxique, i.e. quand les symboles n'ont aucune théorie associée, et aussi modulo une théorie équationnelle arbitraire. Puis nous étendons la notion classique de filtrage entre les motifs et les termes clos au filtrage entre les anti-patterns et les termes clos (anti-filtrage). S'inspirant de l'expressivité des règles de production, nous proposons plusieurs extensions aux constructions de filtrage fournies par Tom. Par conséquent, la condition pour l'application d'une règle n'est plus une simple contrainte de filtrage, mais une combinaison (conjonction ou disjonction) de contraintes de filtrage et d'anti-filtrage ainsi que d'autres types de conditions. Les techniques classiques de compilation du filtrage ne sont pas bien adaptées à ces conditions complexes. Ceci a motivé l'étude d'une nouvelle méthode de compilation basée sur des systèmes de réécriture. L'application de ces systèmes est contrôlée par des stratégies, permettant la mise en place d'extensions futures (comme la prise en compte de nouvelles théories de filtrage) de manière simple et naturelle, sans interférer avec le code existant. Nous avons complètement réécrit le compilateur de Tom en utilisant cette technique. Une fois tous ces éléments rassemblés, on obtient un environnement pour décrire et implémenter des transformations de manière élégante et concise. Pour promouvoir son utilisation dans des projets complexes du milieu industriel, nous développons une technique pour extraire de manière automatique des informations structurelles à partir d'une hiérarchie arbitraire de classes Java. Cela permet l'intégration du filtrage offert par Tom dans n'importe quelle application Java, nouvelle ou déjà existante.

Nautile est un environnement de génération de dessins de masques, adapte aux besoins des compilateurs de silicium. Il permet la réalisation d'outils d'assemblage et de générateurs paramétrés par la technologie. Nautile facilite la décomposition d'un circuit en une hiérarchie de cellules pouvant être formalisées suivant plusieurs niveaux d'abstraction appelés vues. Une cellule possède deux types de vues, les vues physiques et une vue de construction. Celle-ci permet de concevoir des circuits corrects par construction, et met en œuvre des règles de composition paramétrées par la technologie. Enfin, Nautile permet l'intégration d'outils et de cellules développés dans d'autres systèmes

Fp2 (functional parallel programming) est un langage qui concilie programmation fonctionnelle et programmation parallèle a travers le formalisme des spécifications algébriques et des systèmes de réécriture. Dans le cadre du projet fp2, cette thèse a pour principal objectif de présenter la partie fonctionnelle, incluant la généricité et le traitement des exceptions. La généricité (paramétrisation d'une spécification) est traitée dans la première partie: nous rappelons les principes, étudions la sémantique, formalisons la compilation des opérateurs génériques en restant dans un cadre fonctionnel, et analysons les raccourcis de notation offerts aux utilisateurs. La deuxième partie est consacrée aux exceptions. Elles sont d'abord étudiées d'un point de vue opérationnel, puis nous en donnons une définition précise qui permet de ramener une présentation avec exceptions a une présentation avec sortes ordonnées. Cette définition assure l'existence d'une algèbre initiale et permet en outre de traiter les exceptions avec paramètres génériques. En troisième partie, sont présentées des méthodes de transformation de définitions fonctionnelles récursives en processus parallèles communicants. La généricité est utilisée pour formuler les hypothèses sur les définitions fonctionnelles, et nous montrons de plus comment simuler une pile de récursivité de profondeur arbitraire par des réseaux de processus dont la topologie est fixée statiquement

L'objet de cette thèse est la conception d'outils pour l'automatisation du processus de conception d'outils pour l'automatisation du processus de conception des circuits intégrés. Ces outils sont appelés compilateurs de silicium. Le premier chapitre décrit brièvement le contexte de cette thèse. Le second chapitre est une introduction générale a la compilation de silicium. La deuxième partie de la thèse est consacrée aux compilateurs de comportements, ils permettent de générer l'architecture d'un circuit en partant de sa description comportementale. Les techniques mises en œuvre par ces compilateurs sont discutées dans le troisième chapitre. Le quatrième chapitre présente le compilateur de silicium Syco. Syco permet de générer la description physique d'un circuit en partant de sa description comportementale. Le processus de compilation a été simplifie par l'utilisation d'un certain nombre de modelès pre-definis. Les circuits générés sont composes d'une partie opérative parallèle et d'une partie contrôle hiérarchique

Cette étude met en évidence l'utilité des modes directionnels pour l'optimisation de la résolution dans le langage Prolog. Ils se caractérisent essentiellement par le fait qu'ils permettent de distinguer les différentes utilisations possibles d'un même prédicat. Un algorithme de production automatique de ces modes est décrit. L'étude est concrétisée par la réalisation du compilateur Starlog, fonctionnant sur un cas particulier de modes directionnels

Théorèmes de points fixes dans les treillis complets, étude du comportement d'un système dynamique discret, analyse sémantique exacte des programmes et applications. Méthodes constructives d'approximation de points fixes d'opérateurs monotone sur un treillis complet. Analyse sémantique approchée des programmes et applications. Analyse sémantique des procédures recursives.