UCLA

Cyber-Physical Systems (CPSs) are complex systems resulting from intricate interaction of digital computational devices with the physical systems. With the recent dazzling advances in computational devices, CPSs have become ubiquitous in modern technology. The increasing presence of CPSs on one hand and the incapability of current methods to analyze them on the other hand, impel the development of novel approaches for analysis and design. In CPSs, embedded computers have the responsibility of monitoring and controlling the physical plants using feedback loops using which physical plants affect computations and vice versa. In these closed-loop fashions, controllers implemented in software are termed embedded control software.

Increasing use of embedded control software in life critical applications, such as aircraft flight control systems and automotive engine control systems, demands lots of efforts on software verifications and validations which are very costly. On the other hand, by changing the center of gravity from verification to design, it is possible to synthesize correct-by-design embedded control software while providing formal guarantees of correctness. The foundation of this proposed approach relies on some technical results showing how to construct equivalent finite state models for differential equation models describing physical plant. These finite state models are simpler descriptions of physical plant in which

each state of the finite model represents a collection or aggregate of states in the physical plant. Similar finite state models are used in software and hardware modeling, which enable the composition of such models with the finite models of the physical systems. The results of this composition are finite models capturing the behavior of the physical systems interacting with the digital computation devices. Once such models are

available, the methodologies and tools developed in computer science for verification and control synthesis purposes can be easily employed to physical systems, via these models. In the first part of this thesis I take an important step in my quest to synthesize correct-by-design embedded control software for CPSs by constructing finite state models for control systems. I propose a novel technique to compute bisimilar finite state models of incrementally stable nonlinear control systems. I show on practical examples that the finite state models computed by my procedure can be several orders of magnitude smaller than existing approaches. Moreover, I propose another technique to compute (not necessarily bisimilar) finite state models of any nonlinear control system as long as I am interested in its behavior in a compact set. In the second part of this thesis I will show some incremental properties under which nonlinear control systems admit finite state models. I propose some analysis tools to check those properties. Moreover, I provide some design techniques providing controllers enforcing those incremental properties for some special classes of nonlinear control systems.