Les systèmes cyber-physiques sont une classe de systèmes complexe, de grande échelle, souvent critiques de sûreté, qui apparaissent dans des applications industrielles variées. Des approches de vérification formelle sont capable de fournir des garanties pour la performance et la sûreté de ces systèmes. Elles nécessitent trois éléments : un modèle formel, une méthode de vérification, ainsi qu’un ensemble de spécifications formelles. En revanche, les modèles industriels sont typiquement informels, ils sont analysés dans des environnements de simulation informels et leurs spécifications sont décrits dans un langage naturel informel. Dans cette thèse, nous visons à faciliter l’intégration de la vérification formelle dans le processus industriel de la conception basé sur modèle.Notre première contribution clé est une méthodologie de transformation de modèle. A partir d’un modèle de simulation standard, nous le transformons en un modèle de vérification équivalent, plus précisément en un réseau d’automates hybrides. Le processus de transformation prend en compte des différences de syntaxes, sémantique et d’autres aspects de la modélisation. Pour cette classe de modèle formel, des algorithmes d’atteignabilité peuvent être appliqués pour vérifier des propriétés de sûreté. Un obstacle est que des algorithmes d’atteignabilité se mettent à l’échelle pour des modèles affines par morceaux, mais pas pour des modèles non linéaires. Pour obtenir des surapproximations affines par morceaux des dynamiques non linéaires, nous proposons une technique compositionnelle d’hybridisation syntaxique. Le résultat est un modèle très compact qui retient la structure modulaire du modèle d’origine de simulation, tout en évitant une explosion du nombre de partitions.La seconde contribution clé est une approche pour encoder des spécifications formelles riches de façon à ce qu’elles peuvent être interprétées par des outils d’atteignabilité. Nous prenons en compte des spécifications exprimées sous forme d’un gabarit de motif (pattern template), puisqu’elles sont proche au langage naturel et peuvent être compris facilement par des utilisateurs non experts. Nous fournissons (i) des définitions formelles pour des motifs choisis, qui respectent la sémantique des automates hybrides, et (ii) des observateurs qui encodes les propriétés en tant qu’atteignabilité d’un état d’erreur. En composant ces observateurs avec le modèle formel, les propriétés peuvent être vérifiées par des outils standards de vérification qui sont automatisés.Finalement, nous présentons une chaîne d’outils semi-automatisée ainsi que des études de cas menées en collaboration avec des partenaires industriels. / Cyber-Physical Systems form a class of complex, large-scale systems of frequently safety-critical nature in various industrial applications. Formal verification approaches can provide performance and safety guarantees for these systems. They require three elements: a formal model, a formal verification method, and a set of formal specifications. However, industrial models are typically non-formal, they are analyzed in non-formal simulation environments, and their specifications are described in non-formal natural language. In this thesis, we aim to facilitate the integration of formal verification into the industrial model-based design process.Our first key contribution is a model transformation methodology. Starting with a standard simulation model, we transform it into an equivalent verification model, particularly a network of hybrid automata. The transformation process addresses differences in syntax, semantics, and other aspects of modeling. For this class of formal models, so-called reachability algorithms can be applied to verify safety properties. An obstacle is that scalable algorithms exist for piecewise affine (PWA) models, but not for nonlinear ones. To obtain PWA over-approximations of nonlinear dynamics, we propose a compositional syntactic hybridization technique. The result is a highly compact model that retains the modular structure of the original simulation model and largely avoids an explosion in the number of partitions.The second key contribution is an approach to encode rich formal specifications so that they can be interpreted by tools for reachability. Herein, we consider specifications expressed by pattern templates since they are close to natural language and can be easily understood by non-expert users. We provide (i) formal definitions for select patterns that respect the semantics of hybrid automata, and (ii) monitors which encode the properties as the reachability of an error state. By composing these monitors with the formal model under study, the properties can be checked by off-the-shelf fully automated verification tools.Furthermore, we provide a semi-automated toolchain and present results from case studies conducted in collaboration with industrial partners.

Sistemas Supervisórios Híbridos podem ser definidos como sistemas de controle cujos estados são representados por variáveis discretas e contínuas, e cuja dinâmica é determinada em função do tempo e da ocorrência de eventos discretos. O desenvolvimento desta classe de Sistemas Supervisórios pode ser dividido em duas fases. A 1ª Fase consiste na elaboração de um modelo protótipo para o Sistema Supervisório, que é descrito usando um formalismo, e que é validado com base nas especificações do problema. Na 2ª Fase, este modelo, já validado, é convertido na linguagem de programação do Sistema Supervisório propriamente dito. Esta tese concentra-se na 1ª Fase, para qual abordam-se três questões principais: (1) a escolha do formalismo de modelagem; (2) como construir o modelo do Sistema Supervisório Híbrido usando este formalismo; e (3) como validar o Sistema Supervisório Híbrido usando o modelo construído. Para questão (1), introduz-se um novo formalismo de modelagem baseado na aplicação dos conceitos de Orientação a Objetos (OO) às redes Predicado Transição Diferenciais (redes PTD). Este novo formalismo é chamado de redes PTD-OO. No que se refere a questão (2), é proposto um procedimento para obtenção do modelo do Sistema Supervisório em redes PTD-OO usando os diagramas da UML (‘Unified Modeling Language’). Finalmente, para a questão (3), o problema de validação é abordado através da definição de um conjunto de propriedades que o modelo em redes PTD-OO deve respeitar afim de que sejam garantidos os requisitos do Sistema Supervisório. Estas propriedades são, então, verificadas através de um procedimento proposto para análise de redes PTD-OO. / Hybrid Supervisory Systems can be described as control systems with states that are represented by both discrete and continuous variables. Their dynamics are function of time and depend also on the occurrence of discrete events. The development of Hybrid Supervisory Systems can be divided in two phases. In the 1st Phase, a prototype-model for the Supervisory System is described using a specific formalism and is validated based on the system requirements. In the 2nd Phase, this validated model is converted to the programming language of the Supervisory System. This thesis is focused on the 1st Phase of Hybrid Supervisory System development. It approaches three main issues: (1) the choice of the modelling formalism; (2) how to build the Hybrid Supervisory System model using this formalism; and (3) how to validate the Hybrid Supervisory System using this model. For issue (1), a new modelling formalism is introduced based on Differential Predicate Transition nets (DPT nets) and object-oriented (OO) paradigm. This new formalism is called DPT-OO net. Then, for the issue (2), a modelling procedure that assists the building of the DPT-OO net model using Unified Modelling Language (UML) diagrams is proposed. Finally, for the issue (3), the validation problem is approached by defining a set of properties of the DPT-OO net model that assures the Supervisory System requirements. These properties are then formally verified using a proposed analysis procedure.

At present many remote and Island communities rely solely on diesel powered generators to provide electricity. Diesel fuel is both expensive and polluting and the constant speed operation of the diesel engine is inefficient. In this thesis the use of renewable energy sources to help offset diesel fuel usage and an alternative way of running the diesel generator with the aim of reducing electrical energy costs is investigated. Diesel generators have to be sized to meet peak demand, in one or two diesel generator island grids, these generators will be running at a fraction of maximum output for most of the time. A new variable speed diesel generator allows for a reduction in fuel consumption at part load compared to constant speed operation. Combining the variable speed diesel generator with renewable generation should maximise the diesel fuel offsetting of the renewable source due to the increased efficiency at low loads. The stability issues of maintaining transient performance in a renewable variable speed hybrid system have been modelled and simulated. A control strategy has been developed and the use of energy storage as a buffer for any remaining stability problems has been explored. The control strategy has then been experimentally tested along with one of the possible energy storage solutions. An economic feasibility study has been performed on a case study community to validate the main aim of this research of reducing the cost of electrical energy in diesel generator grids.

O conceito de controle híbrido é aplicado à operação de alívio entre um FPWSO e um navio aliviador. Ambos os navios mantêm suas posições e aproamentos pelo resultado da ação do seu Sistema de Posicionamento Dinâmico (SPD). O alívio dura cerca de 24 horas para ser concluído. Durante este período, o estado de mar pode se alterar e os calados estão sendo constantemente alterados. Um controlador híbrido é projetado para permitir modificacões dos parâmetros de controle/observação se alguma alteração significante do estado de mar e/ou calado das embarcações ocorrer. O principal objetivo dos controladores é manter o posicionamento relativo entre os navios com o intuito de evitar perigosa proximidade ou excesso de tensão no cabo. Com isto em mente, uma nova estratégia de controle que atue integradamente em ambos os navios é proposta baseda em geometria diferencial. Observadores não lineares baseados em passividade são aplicados para estimar a posição, a velocidade e as forças externas de mares calmos até extremos. O critério para troca do controle/observação é baseado na variação do calado e no estado de mar. O calado é assumido conhecido e o estado de mar é estimado pela frequência de pico do espectro do movimento de primeira ordem dos navios. Um modelo de perturbação é proposto para encontrar o número de controladores do sistema híbrido. A equivalência entre o controle geométrico e o controlador baseado em Multiplicadores de Lagrange é demonstrada. Assumindo algumas hipóteses, a equivalência entre os controladores geométrico e o PD é também apresentada. O desempenho da nova estratégia é avaliada por meio de simulações numéricas e comparada a um controlador PD. Os resultados apresentam muito bom desempenho em função do objetivo proposto. A comparação entre a abordagem geométrica e o controlador PD aponta um desempenho muito parecido entre eles. / The hybrid control concept is applied to the offoading operation by means of a Floating, Production, Working, Storage and Offoading (FPWSO) vessel and a Shuttle Tanker (ST). Both vessels are able to maintain their position and heading as a result of the Dynamic Positioning System (DPS). The vessels are in tandem configuration connected by a hawser. The offloading operation lasts approximately 24 hours. During this period, the sea condition may change and the drafts are being constantly altered. Hybrid controller is designed to permit modification of the controller/observer parameters should a significant sea state alteration and/or draft variation occur. The main goal of the controllers is to maintain relative positioning between vessels in order to avoid dangerous proximity or excessive hawser tension. With that in mind, a new control strategy is proposed based on dierential geometry that acts integrally in both vessels. Nonlinear observers based on passivity are used to estimate position, velocity and external force ranging from calm to extreme seas. The criterion for changing the controller/observer law is based on draft and sea state. The draft is assumed to be known and sea state is estimated by tracking the peak-frequency of the first-order vessel motion spectrum. A perturbation-based model is proposed to find the number of hybrid system controllers. The equivalence between the geometric control approach and the Lagrange Multiplier (LM) - based control is demonstrated. Taking some assumptions as given, the equivalence between geometric and PD-like controllers is regarded as having also been demonstrated. The performance of the new strategy is assessed by means of numerical simulations and compared to a Proportional-Derivative (PD)-like control. The results present a very good performance as regards the proposed main goal. Result comparison of the geometric approach and the PD-like control shows very similar behavior between geometric and PD-like controllers.

This dissertation studies the application of several event-driven control schemes in multi-agent systems. First, a new cooperative receding horizon (CRH) controller is designed and applied to a class of maximum reward collection problems. Target rewards are time-variant with finite deadlines and the environment contains uncertainties. The new methodology adapts an event-driven approach by optimizing the control for a planning horizon and updating it for a shorter action horizon. The proposed CRH controller addresses several issues including potential instabilities and oscillations. It also improves the estimated reward-to-go which enhances the overall performance of the controller. The other major contribution is that the originally infinite-dimensional feasible control set is reduced to a finite set at each time step which improves the computational cost of the controller. Second, a new event-driven methodology is studied for trajectory planning in multi-agent systems. A rigorous optimal control solution is employed using numerical solutions which turn out to be computationally infeasible in real time applications. The problem is then parameterized using several families of parametric trajectories. The solution to the parametric optimization relies on an unbiased estimate of the objective function's gradient obtained by the "Infinitesimal Perturbation Analysis" method. The premise of event-driven methods is that the events involved are observable so as to "excite" the underlying event-driven controller. However, it is not always obvious that these events actually take place under every feasible control in which case the controller may be useless. This issue of event excitation, which arises specially in multi-agent systems with a finite number of targets, is studied and addressed by introducing a novel performance measure which generates a potential field over the mission space. The effect of the new performance metric is demonstrated through simulation and analytical results.

The thesis has been conducted at Bosch Thermoteknik AB and its aim is to develop a Model Predictive Control (MPC) controller for a ground source heat pump which minimizes the power consumption while being able to keep the inside air temperature and Domestic Hot Water (DHW) temperature within certain comfortintervals. First a model of the system is derived, since the system consists of both continuous and binary states a hybrid model is used. The MPC controller utilizes the model to predict the future states of the system, and by formulating an optimizationproblem an optimal control is achieved. The MPC controller is evaluated and compared to a conventional controller using simulations. After some tuning the MPC controller is capable of maintaining the inside air and DHW temperature at their reference levels without oscillating too much. The MPC controller’s general performance is quite similar to the conventional controller, but with a power consumption which is 1-3 % lower. A simulation using an inside air temperature reference which is lowered during the night is also conducted, it achieved a power consumption which was 7.5 % lower compared to a conventional controller.

Multi-agent systems represent a group of agents that cooperate to solve common tasks in a dynamic environment. Multi-agent control systems have been widely studied in the past few years. The control of multi-agent systems relates to synthesizing control schemes for systems which are inherently distributed and composed of multiple interacting entities. Because of the wide applications of multi-agent theories in large and complex control systems, it is necessary to develop a framework to simplify the process of developing control schemes for multi-agent systems. <br /><br /> In this study, a framework is proposed for the distributed control and coordination of multi-agent systems. In the proposed framework, the control of multi-agent systems is regarded as achieving decentralized control and coordination of agents. Each agent is modeled as a Coordinated Hybrid Agent (CHA) which is composed of an intelligent coordination layer and a hybrid control layer. The intelligent coordination layer takes the coordination input, plant input and workspace input. After processing the coordination primitives, the intelligent coordination layer outputs the desired action to the hybrid layer. In the proposed framework, we describe the coordination mechanism in a domain-independent way, as simple abstract primitives in a coordination rule base for certain dependency relationships between the activities of different agents. The intelligent coordination layer deals with the planning, coordination, decision-making and computation of the agent. The hybrid control layer of the proposed framework takes the output of the intelligent coordination layer and generates discrete and continuous control signals to control the overall process. In order to verify the feasibility of the proposed framework, experiments for both heterogeneous and homogeneous Multi-Agent Systems (MASs) are implemented. In addition, the stability of systems modeled using the proposed framework is also analyzed. The conditions for asymptotic stability and exponential stability of a CHA system are given. <br /><br /> In order to optimize a Multi-Agent System (MAS), a hybrid approach is proposed to address the optimization problem for a MAS modeled using the CHA framework. Both the event-driven dynamics and time-driven dynamics are included for the formulation of the optimization problem. A generic formula is given for the optimization of the framework. A direct identification algorithm is also discussed to solve the optimization problem.

The goal of the proposed research is to provide efficient methods for defining, selecting and encoding multi-modal control programs. To this end, modes are recovered from system observations, i.e. quantized input-output strings are converted into consistent mode sequences within the Motion Description Language (MDL) framework. The design of such modes can help identify and predict the behaviors of complex systems (e.g. biological systems such as insects) and inspire the design and control of robust semi-autonomous systems (e.g. navigating robots). In this work, the efficiency of a method will be defined by the complexity and expressiveness of specific control programs. The insistence on low-complexity programs is originally motivated by communication constraints on the computer control of semi-autonomous systems, but also by our belief that, as complex as they may look, natural systems indeed use short motion schemes with few basic behaviors. The attention is first focused on the design of such short-length, few-distinct-modes mode sequences within the MDL framework. Optimal control problems are then addressed. In particular, given a mode sequence, the question of deciding when the system should switch from one mode to another in order to achieve some reachability requirements is studied. Finally, we propose to investigate how sampling strategies affect complexity and reachability, and how an acceptable trade-off between these conflicting entities can be reached.

As control systems are becoming more and more complex, system complexity is rapidly becoming a limiting factor in the efficacy of established techniques for control systems design. To cope with the growing complexity, control architectures often have a hierarchical structure. At the base of the system pyramid lie feedback loops with simple closed-loop control laws. These are followed, at a higher level, by discrete control logics. Such hierarchical systems typically have a hybrid nature. A common approach to addressing these types of complexity consists of decomposing, in the time domain, the control task into a number of modes, i.e. control laws dedicated to carrying out a limited task. This type of control generally involves switching laws among the various modes, and its design poses a major challenge in many application domains. The primary goal of this thesis is to develop a unified framework for addressing this challenge. To this end, the contribution of this thesis is threefold: 1. An algorithmic framework for how to optimize the performance of switched autonomous systems is derived. The optimization concerns both the sequence in which different modes appear in and the duration of each mode. The optimization algorithms are presented together with detailed convergence analyses. 2. Control strategies for how to optimize switched autonomous systems operating in real time, and when the initial state of the system is unknown, are presented. 3. A control strategy for how to optimally navigate an autonomous mobile robot in real-time is presented and evaluated on a mobile robotics platform. The control strategy uses optimal switching surfaces for when to switch between different modes of operations (behaviors).

The dynamic response and bifurcations of a harmonic oscillator with a hysteretic restoring force and sinusoidal excitation are investigated. A multilinear model of hysteresis is presented. A hybrid system approach is used to formulate and study the problem. A novel method for obtaining exact transient and steady state response of the system is discussed. Simple periodic orbits of the system are analyzed using the KBM method and an analytic criterion for existence of bound and unbound resonance is derived. Results of KBM analysis are compared with those from numerical simulations. Stability and bifurcations of higher period orbits are studied using Poincar´e maps. The Poincar´e map for the system is constructed by composing the corresponding maps for the individual subsystems of the hybrid system. The novelty of this work lies in a.) the study of a multilinear model of hysteresis, and, b.) developing a methodology for obtaining the exact transient and steady state response of the system.