Un logiciel critique est un logiciel dont le mauvais fonctionnement peut avoir un impact important sur la sécurité ou la vie des personnes, des entreprises ou des biens.L'ingénierie logicielle pour les systèmes critiques est particulièrement difficile et combine différentes méthodes pour garantir la qualité des logiciels produits.Parmi celles-ci, les méthodes formelles peuvent être utilisées pour prouver qu'un logiciel respecte ses spécifications.Le travail décrit dans cette thèse s'inscrit dans le contexte de la validation de propriétés de sûreté de programmes critiques, et plus particulièrement des propriétés numériques de logiciels embarqués dans des systèmes de contrôle-commande.La première partie de cette thèse est consacrée aux preuves de stabilité au sens de Lyapunov.Ces preuves s'appuient sur des calculs en nombres réels, et ne sont pas valables pour décrire le comportement d'un programme exécuté sur une plateforme à arithmétique machine.Nous présentons un cadre théorique générique pour adapter les arguments des preuves de stabilité de Lyapunov aux arithmétiques machine.Un outil effectue automatiquement la traduction de la preuve en nombres réels vers une preuve en nombres a virgule flottante.La seconde partie de la thèse porte sur l'analyse des relations affines, en utilisant une interprétation abstraite basée sur l'approximation des valuations associées aux points de contrôle d'un programme par des polyèdres convexes.Nous présentons ALICe, un framework permettant de comparer différentes techniques de génération d'invariants.Il s'accompagne d'une collection de cas de tests tirés de publications sur l'analyse de programmes, et s'interface avec trois outils utilisant différents algorithmes de calcul d'invariants: Aspic, iscc et PIPS.Afin d'affiner les résultats de PIPS, deux techniques de restructuration de code sont introduites, et plusieurs améliorations sont apportées aux algorithmes de génération d'invariants et évaluées à l'aide d'ALICe. / A critical software is a software whose malfunction may result in death or serious injury to people, loss or severe damage to equipment or environmental harm.Software engineering for critical systems is particularly difficult, and combines different methods to ensure the quality of produced software.Among them, formal methods can be used to prove that a software obeys its specifications.This thesis falls within the context of the validation of safety properties for critical software, and more specifically, of numerical properties for embedded software in control-command systems.The first part of this thesis deals with Lyapunov stability proofs.These proofs rely on computations with real numbers, and do not accurately describe the behavior of a program run on a platform with machine arithmetic.We introduce a generic, theoretical framework to adapt the arguments of Lyapunov stability proofs to machine arithmetic.A tool automatically translates the proof on real numbers to a proof with floating-point numbers.The second part of the thesis focuses on linear relation analysis, using an abstract interpretation based on the approximation by convex polyhedrons of valuations associated with each control point in a program.We present ALICe, a framework to compare different invariant generation techniques.It comes with a collection of test cases taken from the program analysis literature, and interfaces with three tools, that rely on different algorithms to compute invariants: Aspic, iscc and PIPS.To refine PIPS results, two code restructuring techniques are introduced, and several improvements are made to the invariant generation algorithms and evaluated using ALICe.

Les interfaces haptiques à retour d’effort sont des dispositifs robotiques capables deproduire des forces à destination de l’utilisateur en téléopération et en réalité virtuelle. L’utilisation d’interface à retour d’effort en Conception Assistée par Ordinateur (CAO) offre de nouvelles perspectives pour la création et la conception de formes 3D grâce à une interactivité à la fois visuelle et kinesthésique. Elles permettent à la fois de visualiser, de manipuler en temps réel des objets virtuels et d’en ressentir les efforts (liés aux contacts, à la déformation, etc.).Les travaux présentés dans cette thèse contribuent au développement d’interfaces àretour d’effort pour répondre au mieux aux besoins de la CAO. Dans ce mémoire, l’accent est placé sur la problématique de la stabilité et son exploitation pour la commande de l’interface mais aussi pour la conception électromécanique. L’ensemble des travaux porte sur une interface à un degré de liberté.Dans un premier temps, différents facteurs liés au système mécanique (amortissement, modes vibratoires) et à l’environnement virtuel (échantillonnage, retard. . .) agissant sur la stabilité d’une interface sont mis en évidence à l’aide de critères fréquentiels. Ensuite, la conception d’une interface (choix et dimensionnement des composants) est ramenée sous forme d’un problème d’optimisation incluant une contrainte liée à la stabilité (en termes de domaine d’utilisation) et un critère de maximisation de la transparence (en termesd’inertie du dispositif).Dans un second temps, l’architecture de commande des dispositifs haptiques est étudiée. À l’aide d’une nouvelle condition de stabilité asymptotique pour les systèmes en temps discret à retard variable et en utilisant un observateur d’état augmenté comme alternative à l’utilisation standard de la méthode des différences finies arrières, la synthèse d’une nouvelle architecture de commande est proposée.La dernière partie du mémoire aborde la description du banc d’essai expérimental développé pendant le travail de thèse ainsi que les résultats des tests réalisés. / Force feedback haptic interfaces are robotic devices which are able to produce forces for the user in a teleoperation or virtual reality context. The integration of force feedback haptic interfaces in Computer-Aided Design (CAD) systems offers new perspectives for modeling and design of 3D objects by combining both visual and kinesthetic interaction. It allows viewing and manipulating virtual objects in real-time with a sense of touch (linked to contact, deformation, etc.).The works presented in this thesis contribute to the development of a force feedbackhaptic device to meet the needs of CAD at the best. In this thesis manuscript, the emphasis is put on the stability issue and its exploitation for the control of the device but also for the electromechanical conception. All the presented works concern an interface with one degree of freedom. First, several factors relative to the mechanic system (physical damping, vibration modes) and to the virtual environment (sampling period, delay-time, etc.) acting on the interface stability are highlighted through frequency domain stability criteria. Then, the interface design (choice and sizing of components) is expressed on the form of an optimization problem including a constraint linked to stability (in terms of application area).In a second part, the control architecture of haptic devices is studied. Using a newstability criterion for systems in discrete time with variable delay and an augmented state observer as an alternative to the standard finite difference scheme, the synthesis of novel control architecture is proposed.The last part of the manuscript deals with the description of the experimental testbench developed during the thesis period together with the results of some realized tests.

[pt] Excitação paramétrica se dá a partir de coeficientes variantes no tempo na dinâmica de um sistema. Este tipo de excitação tem sido um amplo tema de pesquisa desde os campos da mecânica e eletrônica até dinâmica de fluidos. Ela aparece em problemas envolvendo sistemas dinâmicos, por exemplo, como uma forma de controle de vibrações em sistemas auto excitados, tornando este assunto digno de mais investigações. Abordando estabilidade no sentido de Lyapunov, esta dissertação fornece uma base didática de estabilidade desde conceitos básicos, como pontos de equilíbrio e planos de fase, até conceitos mais avançados, como excitação paramétrica e teoria de Floquet. Os objetos de estudo aqui são sistemas lineares com parâmetros periódicos no tempo, o que permite usar a teoria de Floquet para fazer afirmações a respeito da estabilidade da solução trivial do sistema. Vários exemplos são discutidos fazendo uso de um procedimento numérico desenvolvido para construir mapas de estabilidade e planos de fase. Os exemplos apresentados abrangem sistemas mecânicos, eletromagnéticos e eletromecânicos. Fazendo uso de mapas de estabilidade, diversas características de análise de estabilidade são abordadas. Duas estratégias diferentes para avaliar a estabilidade da solução trivial são comparadas: multiplicadores de Floquet e valor máximo dos expoentes característicos de Lyapunov. / [en] Parametric excitation is a type of excitation that arises from timevarying coefficients in a system s dynamics. More specifically, this dissertation deals with time-periodic coefficients. This type of excitation has been an extended topic of research from the fields of mechanics and electronics to fluid dynamics. It appears in problems involving dynamical systems, for example, as a way of controlling vibrations in self-excited systems, making this subject worthy of more investigations. By approaching stability in the sense of Lyapunov, this dissertation provides a didactic stability background from basic concepts, such as equilibrium points and phase diagrams, to more advanced ones, like parametric excitation and Floquet theory. The objects of study here are linear systems with time-periodic parameters. Floquet theory is used to make stability statements about the system s trivial solution. Several examples are discussed by making use of a developed numerical procedure to construct stability maps and phase diagrams. The examples presented herein encompass mechanical, electromagnetic and electromechanical systems. By making use of stability maps, several features that can be discussed in stability analysis are approached. Two different strategies to evaluate the stability of the trivial solution are compared: Floquet multipliers and the maximum value of Lyapunov characteristic exponents.

Este trabalho apresenta o desenvolvimento e as análises de técnicas de controle aplicadas a uma base de movimento de um simulador de vôo. Nos primeiros capítulos são abordados aspectos relacionados com a simulação de movimentos. Uma breve descrição da dinâmica da aeronave e o desenvolvimento do algoritmo de movimento (washout filter) são apresentados. O modelo dinâmico da base de movimento é desenvolvido baseado num manipulador paralelo de seis graus de liberdade chamado de plataforma de Stewart acionado eletricamente. As equações de movimento do atuador eletromecânico são incluídas no modelo dinâmico da plataforma. O controle baseado na dinâmica inversa é uma alternativa para abordar o controle de sistema mecânicos não lineares como a plataforma de Stewart. Porém, essa técnica considera o conhecimento exato do modelo dinâmico do sistema, portanto, a dinâmica não modelada, as incertezas paramétricas e as perturbações externas podem degradar o desempenho do controlador. Além disso, o custo computacional pago pelo cálculo do modelo dinâmico realizado online é muito alto. Nesse contexto, duas estratégias de controle foram aplicadas na malha externa da estrutura de controle baseada na dinâmica inversa para o controle de aceleração na presença de incertezas paramétricas e da dinâmica não modelada, os quais foram introduzidas intencionalmente no processo de aproximar o modelo dinâmico com o objetivo de simplificar a implementação do controle baseado na dinâmica inversa. Na primeira estratégia, o termo robusto de controle foi projetado, provando a estabilidade do sistema linearizado por meio da teoria de estabilidade de Lyapunov. Este controle apresenta o fenômeno conhecido como chattering e então foi adotada uma função de saturação para substituir a lei de controle. Na segunda estratégia, o termo robusto de controle foi projetado considerando um problema de rejeição de distúrbio via controle H \'INFINITO\', onde o controlador considera as incertezas como distúrbios afetando o sistema linearizado resultante da aplicação do controle baseado na dinâmica inversa. Finalmente, três tipos de testes foram realizados para avaliar o sistema de controle: função descritiva, limiar dinâmico e algumas manobras da aeronave calculadas a partir do modelo dinâmico e transformadas através do algoritmo de movimento. As duas estratégias de controle foram comparadas. / This work presents the development and analysis of control techniques applied to a flight simulator motion base. The first chapters deal with subjects related to motion simulation. A brief description of the aircraft dynamic model and the development of the motion algorithm (washout filter) are presented. The motion base dynamics is derived based on a six degree of freedom parallel manipulator driven by electromechanical actuators. The six degree of freedom parallel manipulator is called Stewart platform. The motion equations of the electromechanical actuators are included in the motion base dynamics. Inverse dynamics control is an approach to nonlinear control design, nonetheless, this technique is based on the assumption of exact cancellation of nonlinear terms, therefore, parametric uncertainty, unmodeled dynamics and external disturbances may deteriorate the controller performance. In addition, a high computational burden is paid by computing on-line the complete dynamic model of the motion-base. Robustness can be regained by applying robust control tecniques in the outer loop control structure. In this context, two control strategies were applied in the outer loop of the inverse dynamics control structure linearized system for robust acceleration tracking in the presence of parametric uncertainty and unmodeled dynamic, which are intentionally introduced in the process of approximating the dynamic model in order to simplify the implementation of this approach, the inverse dynamic control. Both control strategies consist of introducing an additional term to the inverse dynamics controller which provides robustness to the control system. In the first strategy, the robust control term was designed proving the stability of the linearized system in the presence of uncertainties, using the Lyapunov stability theory. This control term presents a phenomenon known as chattering. Therefore, a saturation function was adopted to replace the control law. In the second strategy, the robust term was designed for a disturbance rejection problem via H \'INFINITE\' control, where the controller considers the uncertaities as disturbances affecting the linearized system resulting from the application of the inverse dynamic control. Finally, describing function, dynamic threshold and some maneuvers computed from the washout filter were used to evaluate the performance of the controllers. Both approaches were compared.

A teoria de sistemas semidinâmicos impulsivos é um capítulo importante e moderno da teoria de sistemas dinâmicos topológicos. Sistemas impulsivos descrevem processos de evolução que sofrem variações de estado de curta duração e que podem ser consideradas instantâneas. Os sistemas impulsivos admitem vários fenômenos interessantes às vezes, por causa da sua irregularidade, e às vezes por causa da sua regularidade. Para muitos fenômenos naturais, os modelos determinísticos mais realistas são frequentemente descritos por sistemas que envolvem impulsos. Esta teoria vem sendo desenvolvida continuamente. O presente trabalho apresenta resultados originais sobre a teoria de conjuntos minimais, movimentos recorrentes, movimentos quase periódicos e fracamente quase periódicos, teoria de estabilidade de Lyapunov, teoria da quase estabilidade de Zhukovskij e, finalmente, a construção de trajetórias negativas para sistemas semidinâmicos com impulsos. Os resultados novos apresentados neste trabalho estão contidos em três artigos, dos quais dois já foram aceitos para publicação. Veja [13], [14] e [15] / The theory of impulsive semidynamical systems is an important and modern chapter of the theory of topological dynamical systems. Impulsive systems describe the evolution of process whose continuous dynamics are interrupted by abrupt changes of state. This kind of systems admits various interesting phenomena sometimes, because of their irregularity, and sometimes because of their regularity. In many natural phenomena, the real deterministic models are often described by systems which involve impulses. This theory has been developed continuously. This work presents original results involving the theory of minimal sets, recurrent motions, almost periodic and weakly almost periodic motions, the study of Lyapunov stability and Zhukovshij Quasi stability and the construction of negative trajectories for impulsive semidynamical systems. The new results presented in this work are contained in three papers namely [13], [14] and [15]

Hybrid systems with or without stochastic noise and with or without time delay are addressed and the qualitative properties of these systems are investigated. The main contribution of this thesis is distributed in three parts. In Part I, nonlinear stochastic impulsive systems with time delay (SISD) with variable impulses are formulated and some of the fundamental properties of the systems, such as existence of local and global solution, uniqueness, and forward continuation of the solution are established. After that, stability and input-to-state stability (ISS) properties of SISD with fixed impulses are developed, where Razumikhin methodology is used. These results are then carried over to discussed the same qualitative properties of large scale SISD. Applications to automated control systems and control systems with faulty actuators are used to justify the proposed approaches. Part II is devoted to address ISS of stochastic ordinary and delay switched systems. To achieve a variety stability-like results, multiple Lyapunov technique as a tool is applied. Moreover, to organize the switching among the system modes, a newly developed initial-state-dependent dwell-time switching law and Markovian switching are separately employed. Part III deals with systems of differential equations with piecewise constant arguments with and without random noise. These systems are viewed as a special type of hybrid systems. Existence and uniqueness results are first obtained. Then, comparison principles are established which are later applied to develop some stability results of the systems.

The purpose of this thesis is to develop new stability conditions for several linear dynamic systems, including linear parameter-varying (LPV), time-delay systems (LPVTD), slow LPV systems, and parameter-dependent linear time invariant (LTI) systems. These stability conditions are less conservative and/or computationally easier to apply than existing ones. This dissertation is composed of four parts. In the first part of this thesis, the complete stability domain for LTI parameter-dependent (LTIPD) systems is synthesized by extending existing results in the literature. This domain is calculated through a guardian map which involves the determinant of the Kronecker sum of a matrix with itself. The stability domain is synthesized for both single- and multi-parameter dependent LTI systems. The single-parameter case is easily computable, whereas the multi-parameter case is more involved. The determinant of the bialternate sum of a matrix with itself is also exploited to reduce the computational complexity. In the second part of the thesis, a class of parameter-dependent Lyapunov functions is proposed, which can be used to assess the stability properties of single-parameter LTIPD systems in a non-conservative manner. It is shown that stability of LTIPD systems is equivalent to the existence of a Lyapunov function of a polynomial type (in terms of the parameter) of known, bounded degree satisfying two matrix inequalities. The bound of polynomial degree of the Lyapunov functions is then reduced by taking advantage of the fact that the Lyapunov matrices are symmetric. If the matrix multiplying the parameter is not full rank, the polynomial order can be reduced even further. It is also shown that checking the feasibility of these matrix inequalities over a compact set can be cast as a convex optimization problem. Such Lyapunov functions and stability conditions for affine single-parameter LTIPD systems are then generalized to single-parameter polynomially-dependent LTIPD systems and affine multi-parameter LTIPD systems. The third part of the thesis provides one of the first attempts to derive computationally tractable criteria for analyzing the stability of LPV time-delayed systems. It presents both delay-independent and delay-dependent stability conditions, which are derived using appropriately selected Lyapunov-Krasovskii functionals. According to the system parameter dependence, these functionals can be selected to obtain increasingly non-conservative results. Gridding techniques may be used to cast these tests as Linear Matrix Inequalities (LMI's). In cases when the system matrices depend affinely or quadratically on the parameter, gridding may be avoided. These LMI's can be solved efficiently using available software. A numerical example of a time-delayed system motivated by a metal removal process is used to demonstrate the theoretical results. In the last part of the thesis, topics for future investigation are proposed. Among the most interesting avenues for research in this context, it is proposed to extend the existing stability analysis results to controller synthesis, which will be based on the same Lyapunov functions used to derive the nonconservative stability conditions. While designing the dynamic ontroller for linear and parameter-dependent systems, it is desired to take the advantage of the rank deficiency of the system matrix multiplying the parameter such that the controller is of lower dimension, or rank deficient without sacrificing the performance of closed-loop systems.

Many control algorithms for ABS systems have been proposed in the literature since the introduction of this equipment by Bosch in 1978. In general, one can divide these control algorithms into two different types: those based on a regulation logic with wheel acceleration thresholds that are used by most commercial ABS systems; and those based on wheel slip control that are preferred in the large majority of academic algorithms. Each approach has its pros and cons [Shida 2010]. Oversimplifying, one can say that the strength of the first ones is their robustness; while that of the latter ones their short braking distances (on dry grounds) and their absence of limit cycles. At the midpoint of this industry/academy dichotomy, based on the concept of extended braking stiffness (XBS), a quite different class of ABS control strategies has been proposed by several researchers (see, e.g., [Sugai 1999] and [Ono 2003]). This concept combines the advantages from both the industrial and academic approaches. Nevertheless, since the slope of the tyre characteristic is not directly measurable, it introduces the question of real-time XBS estimation. The first part of this thesis is devoted to the study of this estimation problem and to a generalization of the proposed technique to a larger class of systems. From the technological point of view, the design of ABS control systems is highly dependent on the ABS system characteristics and actuator performance. Current ABS control algorithms on passenger cars, for instance the Bosch ABS algorithm, are based on heuristics that are deeply associated to the hydraulic nature of the actuator. An interesting observation is that they seem to work properly only in the presence of a specific delay coming from the hydraulic actuation [Gerard 2012]. For brake systems that have different delays compared to those of hydraulic actuators, like electric in-wheel motors (with a smaller delay) or pneumatic trailer brakes (with a bigger delay), they might be no longer suitable [Miller 2013]. Therefore, adapting standard ABS algorithms to other advanced actuators becomes an imperative goal in the automobile industry. This goal can be reached by the compensation of the delays induced by actuators. The second part of this thesis is focused on this issue, and to the generalization of the proposed technique to a particular class of nonlinear systems. Throughout this thesis, we employ two different linearization techniques: the linearization of the error dynamics in the construction of model-based observers [Krener 1983] and the linearization based on restricted state feedback [Brockett 1979]. The former is one of the simplest ways to build an observer for dynamical systems with output and to analyze its convergence. The main idea is to transform the original nonlinear system via a coordinate change to a special form that admits an observer with a linear error dynamics and thus the observer gains can be easily computed to ensure the observer convergence. The latter is a classical method to control nonlinear systems by converting them into a controllable linear state equation via the cancellation of their nonlinearities. It is worth mentioning that existing results for observer design by error linearization in the literature are only applied to the case of regular time scalings ([Guay 2002] and [Respondek 2004]). The thesis shows how to extend them to the case of singular time scalings. Besides, the thesis combines the classical state feedback linearization with a new method for the input delay compensation to resolve the output tracking problem for restricted feedback linearizable systems with input delays.

Hybrid systems with or without stochastic noise and with or without time delay are addressed and the qualitative properties of these systems are investigated. The main contribution of this thesis is distributed in three parts. In Part I, nonlinear stochastic impulsive systems with time delay (SISD) with variable impulses are formulated and some of the fundamental properties of the systems, such as existence of local and global solution, uniqueness, and forward continuation of the solution are established. After that, stability and input-to-state stability (ISS) properties of SISD with fixed impulses are developed, where Razumikhin methodology is used. These results are then carried over to discussed the same qualitative properties of large scale SISD. Applications to automated control systems and control systems with faulty actuators are used to justify the proposed approaches. Part II is devoted to address ISS of stochastic ordinary and delay switched systems. To achieve a variety stability-like results, multiple Lyapunov technique as a tool is applied. Moreover, to organize the switching among the system modes, a newly developed initial-state-dependent dwell-time switching law and Markovian switching are separately employed. Part III deals with systems of differential equations with piecewise constant arguments with and without random noise. These systems are viewed as a special type of hybrid systems. Existence and uniqueness results are first obtained. Then, comparison principles are established which are later applied to develop some stability results of the systems.

In this dissertation, we present several main research thrusts involving thermodynamic stabilization via energy dissipating hybrid controllers and nonlinear control of network systems. Specifically, a novel class of fixed-order, energy-based hybrid controllers is presented as a means for achieving enhanced energy dissipation in Euler-Lagrange, lossless, and dissipative dynamical systems. These dynamic controllers combine a logical switching architecture with continuous dynamics to guarantee that the system plant energy is strictly decreasing across switching. In addition, we construct hybrid dynamic controllers that guarantee that the closed-loop system is consistent with basic thermodynamic principles. In particular, the existence of an entropy function for the closed-loop system is established that satisfies a hybrid Clausius-type inequality. Special cases of energy-based hybrid controllers involving state-dependent switching are described, and the framework is applied to aerospace system models. The overall framework demonstrates that energy-based hybrid resetting controllers provide an extremely efficient mechanism for dissipating energy in nonlinear dynamical systems. Next, we present finite-time coordination controllers for multiagent network systems. Recent technological advances in communications and computation have spurred a broad interest in autonomous, adaptable vehicle formations. Distributed decision-making for coordination of networks of dynamic agents addresses a broad area of applications including cooperative control of unmanned air vehicles, microsatellite clusters, mobile robotics, and congestion control in communication networks. In this part of the dissertation we focus on finite-time consensus protocols for networks of dynamic agents with undirected information flow. The proposed controller architectures are predicated on the recently developed notion of system thermodynamics resulting in thermodynamically consistent continuous controller architectures involving the exchange of information between agents that guarantee that the closed-loop dynamical network is consistent with basic thermodynamic principles.