Th.--Informatique--Nice, 1988. / 1989 d'après la déclaration de dépôt légal. Bibliogr. p. 160-163. Résumé en français.

Th. doct.--Informatique--Nice, 1996. / Bibliogr. p. 149-161. Résumé en anglais et en français. 1996 d'après la déclaration de dépôt légal.

<p>The use of computer-based systems is rapidly increasing and such systems can now be found in a wide range of applications, including safety-critical applications such as cars and aircrafts. To make the development of such systems more efficient, there is a need for tools for automatic safety analysis, such as analysis of fault tolerance.</p><p>In this thesis, a tool for automatic formal analysis of fault tolerance was developed. The tool is built on top of the existing development environment for the synchronous language Esterel, and provides an output that can be visualised in the Item toolkit for fault tree analysis (FTA). The development of the tool demonstrates how fault tolerance analysis based on formal verification can be automated. The generated output from the fault tolerance analysis can be represented as a fault tree that is familiar to engineers from the traditional FTA analysis. The work also demonstrates that interesting attributes of the relationship between a critical fault combination and the input signals can be generated automatically.</p><p>Two case studies were used to test and demonstrate the functionality of the developed tool. A fault tolerance analysis was performed on a hydraulic leakage detection system, which is a real industrial system, but also on a synthetic system, which was modeled for this purpose.</p>

Embedded controllers coordinate the behaviours of specialised hardware components to satisfy broader application requirements. They are difficult to model and to program. One of the greatest challenges is to express intricate timing behaviours???which arise from the physical characteristics of components???while not precluding efficient implementations on resource-constrained platforms. Aspects of this challenge are addressed by this thesis through four distinct applications of timed automata and the synchronous languages Argos and Esterel. A novel framework for simulating controllers written in an imperative synchronous language is described. It includes a transformation of synchronous models into timed automata that accounts for timing properties which are important in constrained implementations but ignored by the usual assumption of synchrony. The transformation provides an interface between the discrete time of synchronous programs and a continuous model of time. This interface is extended to provide a way for simulating Argos programs within the widely-used Simulink software. Timed automata are well-suited for semantic descriptions, like the aforementioned transformation, and for modelling abstract algorithms and protocols. This thesis also includes a different type of case study. The timing diagram of a small-scale embedded component is modelled in more detail than usual with the aim of studying timing properties in this type of system. Multiple models are constructed, including one of an assembly language controller. Their interrelations are verified in Uppaal using a construction for timed trace inclusion testing. Existing constructions for testing timed trace inclusion do not directly address recent features of the Uppaal modelling language. Novel solutions for the problems presented by selection bindings, quantifiers, and channel arrays in Uppaal are presented in this thesis. The first known implementation of a tool for automatically generating a timed trace inclusion construction is described. The timed automata case study demonstrates one way of implementing application timing behaviours while respecting implementation constraints. A more challenging, but less detailed, example is proposed to evaluate the adequacy of Esterel for such tasks. Since none of the standard techniques are completely adequate, a novel alternative for expressing delays in physical time is proposed. Programs in standard Esterel are recovered through syntactic transformations that account for platform constraints.

The use of computer-based systems is rapidly increasing and such systems can now be found in a wide range of applications, including safety-critical applications such as cars and aircrafts. To make the development of such systems more efficient, there is a need for tools for automatic safety analysis, such as analysis of fault tolerance. In this thesis, a tool for automatic formal analysis of fault tolerance was developed. The tool is built on top of the existing development environment for the synchronous language Esterel, and provides an output that can be visualised in the Item toolkit for fault tree analysis (FTA). The development of the tool demonstrates how fault tolerance analysis based on formal verification can be automated. The generated output from the fault tolerance analysis can be represented as a fault tree that is familiar to engineers from the traditional FTA analysis. The work also demonstrates that interesting attributes of the relationship between a critical fault combination and the input signals can be generated automatically. Two case studies were used to test and demonstrate the functionality of the developed tool. A fault tolerance analysis was performed on a hydraulic leakage detection system, which is a real industrial system, but also on a synthetic system, which was modeled for this purpose.

This dissertation addresses two important problems in reusing intellectual properties (IPs) in the form of reusable design or verification components. The first problem is associated with fast and effective integration of reusable design components into a System-on-chip (SoC), so faster design turn-around time can be achieved, leading to faster time-to-market. The second problem has the same goals of faster product design cycle, but emphasizes on verification model reuse, rather than design component reuse. It specifically addresses reuse of reusable verification IPs to enable a "write once, use many times" verification strategy. This dissertation is accordingly divided into part I and part II which are related but describe the two problems and our solutions to them. These two related but distinctive problems faced by system design companies have been tackled through a unique approach which hither-to-fore only have been used in the software engineering domain. This approach is called metamodeling, which allows creating customized meta-language to describe the syntax and semantics for a modeling domain. It provides a way to create, transform and analyze domain specific languages, which are themselves described by metamodels, and the transformation and processing of models in such languages are also described by metamodels. This makes machine based interpretation and translation from these models an easier and formal task. In part I, we consider the problem of rapid system-level model integration of existing reusable components such that (i) the required architecture of the SoC can be expressed formally, (ii) automatic selection of components from an IP library to match the need of the system being integrated can be done, (iii) integrability of the components is provable, or checkable automatically, and (iv) structural and behavioral type systems for each component can be utilized through inferencing and matching techniques to ensure their compatibility. Our solutions include a component composition language, algorithms for component selection, type matching and inferencing algorithms, temporal property based behavioral typing, and finally a software system on top of an existing metamodeling environment. In part II, we use the same metamodeling environment to create a framework for modeling generative verification IPs. Our main contributions relate to INTEL's microprocessor verification environment, and our solution spans various abstraction levels (System, architectural, and microarchitecture) to perform verification. We provide a unified language that can be used to model verification IPs at all abstraction levels, and verification collaterals such as testbenches, simulators, and coverage monitors can be generated from these models, thereby enhancing reuse in verification. / Ph. D.

This master's thesis deals with a parallel design of the program and a technical equipment of embedded systems. It involves both a general description of the whole process and an illustration of the design, a simulation and implementation of the FIR filter. It also includes a description of the proposed program Polis and the simulation system Ptolemy. The conclusion of the project is devoted to a generation of simulation models in VHDL language incl. a subsequent synthesis.

On parle de plus en plus de systèmes (ou plateformes) reconfigurables qui intègrent sur un même substrat un ou plusieurs cœurs de processeurs et une matrice programmable (ex: Excalibur d'Altera, Virtex 2-Pro et Virtex 4-Fx de Xilinx). Par ailleurs, tout un champ technologique émerge actuellement dans le domaine de la reconfiguration dynamique. Le concepteur se retrouve face à des choix d'implantations logicielles (spécifiques ou génériques) et matérielles (figées ou reconfigurables) pour les différentes parties de l'application. Pour les prochaines générations de systèmes, la complexité croissante nécessite de faire appel à des méthodes et outils d'aide à la prise de décisions. Il est donc nécessaire d'étendre ou de repenser les approches de conception actuelles afin de les adapter aux possibilités offertes par les technologies reconfigurables.<br />Cette thèse propose une méthode automatique de partitionnement logiciel/matériel qui cible des systèmes mixtes logiciel et matériel reconfigurable dynamiquement et a pour objectif de minimiser le temps d'exécution global sous contrainte de surface maximale. Elle offre un flot complet à partir de la spécification au niveau système de l'application (écrite en SSM : formalisme graphique du langage synchrone Esterel) jusqu'à son raffinement vers les outils de niveau RTL. La méthode, basée sur un algorithme génétique, prend en compte les spécificités de l'architecture reconfigurable en ajoutant au partitionnement spatial (ou affectation) classique une étape de partitionnement temporel afin de distribuer dans le temps les configurations successivement implantées sur le reconfigurable. Les performances sont évaluées par une étape d'ordonnancement qui prend en compte les temps de communication et ceux dus aux changements de configurations.

[pt] Apesar da pesquisa contínua para facilitar a programação de redes de sensores sem fio, a análise de perigos de concorrência ainda é de responsabilidade do programador, que deve tratar manualmente de questões como sincronização e memória compartilhada. Nós apresentamos uma linguagem de sistema que garante concorrência segura tratando ameaças em tempo de compilação. A fundamentação estática e síncrona da nossa abordagem permite um raciocínio mais simples sobre questões de concorrência, permitindo uma análise em tempo de compilação que garante programas determinísticos. Como contra-partida, nosso modelo impõe em termos da expressividade da linguagem, tais como para efetuar cálculos demorados, ou atender prazos estritos em tempo real. Nós implementamos diversos protocolos de rede conhecidos e o driver para rádio CC2420 para mostrar que a expressividade e responsividade obtida com a linguagem é suficiente para uma gama considerável de aplicações para redes de sensores. As implementações mostram uma redução de tamanho de código, com um aumento de memória abaixo de 10 porcento em comparação com nesC. O uso da linguagem proposta implica em diversas propriedades de segurança que se baseiam em abstrações de controle de alto nível, também resultando em código mais conciso e legível. / [en] Despite the continous research to facilitate Wireless Sensor Networks development, most safety analysis and mitigation efforts in concurrency are still left to developers, who must manage synchronization and shared memory explicitly. We propose a system language that ensures safe concurrency by handling threats at compile time, rather than at runtime. The synchronous and static foundation of our design allows for a simple reasoning about concurrency that enables compile-time analysis resulting in deterministic and memory-safe programs. As a trade-off, our design imposes limitations on the language expressiveness, such as doing computationally-intensive operations and meeting hard real-time responsiveness. To show that the achieved expressiveness and responsiveness is sufficient for a wide rage of WSN applications, we implement widespread network protocols and the CC2420 radio driver. The implemetations show a reduction in source code size, with a penalty of memory increase below 10 percent in comparison to nesC. Overall, we ensure safety properties for programs relying on high-level control abstractions that also lead to concise and readable code.