As control systems become more integrated with high-end engineering systems as well as consumer products, they are expected to achieve specifications that may include logic rules, safety constraints, startup procedures, and so forth. Control design for such complex specifications is a relatively unexplored research area. One possible design approach is based on partitioning the state space into polytopic regions, and then formulating a certain control problem on each polytope, with the intention that the set of all controllers so obtained would collectively achieve the specification. The control problem which must be solved for each polytope is called the reach control problem, and it has been identified as turnkey to the further development of this approach. The reach control problem (RCP) is to find a state feedback to make the closed-loop trajectories of an affine (or linear) control system defined on a polytope reach and exit a prescribed facet of the polytope in finite time. This dissertation studies a number of aspects of the reach control problem, and it uses tools from convex analysis, nonsmooth analysis, and computational geometry for this study. The dissertation has three main themes. First, we formulate and solve a variant of RCP in which trajectories exit the polytope in a monotonic sense; this provides a triangulation-independent solution of RCP. Second, we develop a Lyapunov-like theory for verifying if RCP is solved using a given candidate controller. This involves the introduction of the notion of generalized flow functions, a LaSalle Principle for RCP, and several converse theorems on existence of generalized flow functions. Third, we study the relationship between affine feedbacks and continuous state feedbacks for RCP on simplices. Although the two feedback classes have been shown to be equivalent under an assumption on the triangulation of the state space, we show by a counterexample that the equivalence is no longer true under arbitrary triangulations. Then we provide for single-input systems a constructive method for the synthesis of multi-affine feedbacks for RCP on simplices.

As control systems become more integrated with high-end engineering systems as well as consumer products, they are expected to achieve specifications that may include logic rules, safety constraints, startup procedures, and so forth. Control design for such complex specifications is a relatively unexplored research area. One possible design approach is based on partitioning the state space into polytopic regions, and then formulating a certain control problem on each polytope, with the intention that the set of all controllers so obtained would collectively achieve the specification. The control problem which must be solved for each polytope is called the reach control problem, and it has been identified as turnkey to the further development of this approach. The reach control problem (RCP) is to find a state feedback to make the closed-loop trajectories of an affine (or linear) control system defined on a polytope reach and exit a prescribed facet of the polytope in finite time. This dissertation studies a number of aspects of the reach control problem, and it uses tools from convex analysis, nonsmooth analysis, and computational geometry for this study. The dissertation has three main themes. First, we formulate and solve a variant of RCP in which trajectories exit the polytope in a monotonic sense; this provides a triangulation-independent solution of RCP. Second, we develop a Lyapunov-like theory for verifying if RCP is solved using a given candidate controller. This involves the introduction of the notion of generalized flow functions, a LaSalle Principle for RCP, and several converse theorems on existence of generalized flow functions. Third, we study the relationship between affine feedbacks and continuous state feedbacks for RCP on simplices. Although the two feedback classes have been shown to be equivalent under an assumption on the triangulation of the state space, we show by a counterexample that the equivalence is no longer true under arbitrary triangulations. Then we provide for single-input systems a constructive method for the synthesis of multi-affine feedbacks for RCP on simplices.

<p>Formal methods such as Event-B are a widely used approach for developing critical systems. This thesis demonstrates that creating models and proving the consistency of the models at the requirements level during software (system) development is an effective way to reduce the occurrence of faults and errors in a practical application. An insulin infusion pump (IIP) is a complicated and time critical system. This thesis uses Event-B to specify models for an IIP, based on a draft requirements document developed by the US Food and Drug Administration (FDA). Consequently it demonstrates Event-B can be used effectively to detect the missing properties, the missing quantities, the faults and the errors at the requirements level of a system development. The IIP is an active and reactive time control system. To achieve the goal of handling timing issues in the IIP system, we made extensions of an existing time pattern specified using Event-B to enrich the semantics of the Event-B language. We created several sets to model the activation times of different events and the union of these time sets defines a global time activation set. The tick of global time is specified as a progress tick event. All the actions in an event are triggered only when the global time in the time tick event matches the time specified in the event. Time is deleted from the corresponding time set, but not the corresponding global time set while the event is triggered. A time point is deleted from the global time set only when there are no pending actions for that time point. Through discharging proof obligations using Event-B, we achieved our goal of improving the requirements document.</p> / Master of Computer Science (MCS)

Autonomous multi-robot systems have found many real-world applications in factory settings, rescue tasks and light shows. Albeit these successful applications, the multi-robot system is usually pre-programmed with limited flexibility for online adaptation. Having a human-in-the-loop feature would provide additional flexibility such as handling unexpected situations, detecting and correcting bad behaviours and supporting the automated decision making. In addition, it would also allow for an extra level of cooperation between the robots and the human that facilitates certain real-world tasks, for example in the agricultural sector. Control barrier functions (CBFs), as a convenient modular-design tool, will be mainly explored. CBFs have seen a lot of development in recent years and extending them to the field of multi-robot systems is still new. In particular, creating an original distributed approach, instead of a centralized one, will be one of the key topics of this Master’s thesis project. In this thesis work, several multi-robot coordination protocols and safety constraints will be identified and these constraints will be enforced using a control barrier function-enabled mixer module. This module will take in the commands from both the planner and the human operator, prioritizing the commands from the human operator as long as the safety constraints are not violated. Otherwise, the mixer module will filter the commands and send out a safe alternative. The underlying multi-robot tasks are expected to be achieved whenever feasible. Simulations in ROS, Python and MATLAB environments are developed to experimentally assess the safety and optimality of the system, and experiments with real robots in a lab are performed to show the applicability of this algorithm. Finally, a distributed approach to the mixer module has been developed, based on previous research and extended to allow for more versatility. This is of key importance since it would allow each robot to compute its own controller based on local information, making the multi-robot system both more robust and flexible to be deployed on real-world applications. / Autonoma multirobotsystem har fått många verkliga tillämpningar i fabriksmiljöer, räddningsuppdrag och ljusshower. Trots dessa framgångsrika tillämpningar är multirobotsystemet vanligtvis förprogrammerat med begränsad flexibilitet för anpassning online. En människa i loopen skulle ge ytterligare flexibilitet, t.ex. när det gäller att hantera oväntade situationer, upptäcka och korrigera dåliga beteenden och stödja det automatiska beslutsfattandet. Dessutom skulle det också möjliggöra en extra samarbetsnivå mellan robotarna och människan som underlättar vissa verkliga uppgifter, till exempel inom jordbrukssektorn. Kontrollbarriärfunktioner (CBF), som ett bekvämt verktyg för modulbaserad utformning, kommer huvudsakligen att undersökas. CBF:er har utvecklats mycket under de senaste åren och det är fortfarande nytt att utvidga dem till flerrobotsystem. Att skapa ett originellt distribuerat tillvägagångssätt i stället för ett centraliserat kommer att vara ett av de viktigaste ämnena i detta examensarbete. I detta examensarbete kommer flera samordningsprotokoll och säkerhetsbegränsningar för flera robotar att identifieras och dessa begränsningar kommer att upprätthållas med hjälp av en mixermodul med kontrollbarriärfunktion. Denna modul kommer att ta emot kommandon från både planeraren och den mänskliga operatören och prioritera kommandon från den mänskliga operatören så länge säkerhetsbegränsningarna inte överträds. I annat fall kommer mixermodulen att filtrera kommandona och skicka ut ett säkert alternativ. De underliggande multirobotuppgifterna förväntas uppnås närhelst det är möjligt. Simuleringar i ROS-, Python- och MATLAB-miljöerna utvecklas för att experimentellt bedöma systemets säkerhet och optimalitet, och experiment med riktiga robotar i ett labb utförs för att visa algoritmens tillämpbarhet. Slutligen har ett distribuerat tillvägagångssätt för mixermodulen utvecklats, baserat på tidigare forskning och utökat för att möjliggöra större mångsidighet. Detta är av central betydelse eftersom det skulle göra det möjligt för varje robot att beräkna sin egen styrning utifrån lokal information, vilket gör systemet med flera robotar både mer robust och flexibelt för att kunna användas i verkliga tillämpningar.