Laurent Fribourg is head of the LSV (Laboratoire Spécification et Vérification) and Scientific Coordinator of the Institut Farman, Institut Fédératif de Recherche CNRS, which brings together the expertise of five laboratories from ENS Cachan, in France, in the fields of modeling, simulation and validation of complex systems. He has published over 70 articles in international journals and reviewed proceedings of international conferences, in the domain of the theory of formal methods and their applications.Romain Soulat is in the third year of his doctorate at the LSV at ENS Cachan in France, under the supervision of Laurent Fribourg. He is working on the modeling and verification of hybrid systems. In particular, his interests concern robustness in scheduling problems – especially as part of a collaborative project with EADS Astrium on the verification of a component in the launcher for the future Ariane 6 rocket. He has published 5 articles in reviewed proceedings of international conferences.

• PREFACE ixACKNOWLEDGMENTS xiINTRODUCTION xiiiCHAPTER 1. CONTROL THEORY: BASIC CONCEPTS  11.1. Model of control systems 11.2. Digital control systems 31.2.1. Digitization 31.2.2. Quantization 61.2.3. Switching 61.3. Control of switched systems using invariant sets 81.3.1. Controlled invariants 91.3.2. Safety control problem 91.3.3. Stability control problem 101.3.4. Other controllers 111.4. Notes 11CHAPTER 2. SAMPLED SWITCHED SYSTEMS 132.1. Model 132.2. Illustrative examples 182.3. Zonotopes 212.4. Notes 23CHAPTER 3. SAFETY CONTROLLERS 253.1. Backward fixed point computation (direct approach) 263.2. Approximate bisimulation (indirect approach) 293.3. Application to a three-cell Boost DC–DC converter 353.3.1. Model 353.3.2. Direct method 373.3.3. Indirect method 373.4. Notes 40CHAPTER 4. STABILITY CONTROLLERS 414.1. Motivation 424.2. Preliminaries 424.2.1. Control induced by the decomposition 454.3. Decomposition function 464.3.1. Basic procedure 464.3.2. Enhancement for safety 484.4. Limit cycles 524.4.1. Discussion of the assumptions H1 and H2 534.4.2. Illustrative examples 544.5. Implementation 584.6. Notes 59CHAPTER 5. APPLICATION TO MULTILEVEL CONVERTERS  615.1. Multilevel converters 625.2. Application of the decomposition procedure 625.2.1. Five-level converter 635.2.2. Seven-level converter 675.3. Physical experimentations 705.4. Notes 73CHAPTER 6. OTHER ISSUES: REACHABILITY, SENSITIVITY, ROBUSTNESS AND NONLINEARITY 756.1. Reachability control 756.2. Sensitivity 786.3. Robust safety control 796.4. Nonlinearity 826.5. Notes 87CONCLUSIONS AND PERSPECTIVES 89APPENDIX 1. SUFFICIENT CONDITION OF DECOMPOSITION 93APPENDIX 2. APPLICATIONS OF THE ENHANCED DECOMPOSITION PROCEDURE 97APPENDIX 3. PROOF OF THEOREM 4.3 103APPENDIX 4. EXAMPLE WITH |R∗Δ| = ∞ 107APPENDIX 5. CODE 109BIBLIOGRAPHY 121INDEX 127