A cyber-physical system tightly coordinates discrete computation and continuous control of physical resources. Most safety-critical cyber-physical systems run sophisticated control algorithms at their core. While these control algorithms have been studied thoroughly from a theoretical standpoint, their implementation on real platforms raises many issues that need to be addressed to ensure the reliability of cyber-physical systems. While control theory studies the properties of a control system based on real analysis and mostly ignores the effect of implementing the control laws in software, these effects can have a significant impact on the performance or stability of the implementation of a control law.

Consider the following mismatches between assumptions made by control theory and guarantees provided by implementation platforms. First, control theoretic methods are based on real analysis, which assume real numbers are infinite-precision. However, in software implementation, mathematical real numbers are approximated using floating-point or fixed-point arithmetic. Second, control computation time is often assumed to be negligible, which may not often be the case in the real implementations. Third, when multiple control applications run on a shared platform, schedulability requirements of the corresponding tasks impose additional constraints on the behavior of the systems, that traditional mathematical control design algorithms do not take into account.

In this thesis, we address these three problems related to implementation of controller software for cyber-physical systems. First, we show how the stability property can be verified for a physical system under the action of controller software and how to synthesize controller software to minimize the effect of quantization error on the stability quality. Second, we show that the naive implementation of some control algorithms may be infeasible due the computation time required for the control tasks on real platforms and provide a memoization based implementation scheme that guarantees the feasibility of the implementation along with maintaining expected control performance. Third, we address the problem of scheduling control tasks from multiple control systems on a single processor and provide static and dynamic scheduler synthesis strategies to maintain stability and achieve optimal performance in the control systems. Solving these problems takes an important step towards closing the gap between control theory and the implementation of control systems.

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.