1: \begin{abstract}

2: Software implementations of controllers for physical systems are at the core of many embedded systems.

3: The design of controllers uses the theory of dynamical systems to construct a 

4: mathematical control law that ensures that the controlled system has certain properties, 

5: such as asymptotic convergence to an equilibrium point, while optimizing some performance criteria.

6: However, owing to quantization errors arising from the use of fixed-point arithmetic,

7: the implementation of this control law can only guarantee

8: {\em practical} stability: under the actions of the implementation, the trajectories

9: of the controlled system converge to a bounded set around the equilibrium point, and the

10: size of the bounded set is proportional to the error in the implementation.

11: The problem of verifying whether a controller implementation achieves practical stability

12: for a given bounded set has been studied before.

13: In this paper, we change the emphasis from verification to automatic {\em synthesis}. 

14: Using synthesis, the need for formal verification can be considerably reduced thereby reducing 

15: the design time as well as design cost of embedded control software. 

16: 

17: We give a methodology and a tool to synthesize embedded control 

18: software that is Pareto optimal

19: w.r.t.\ both performance criteria and practical stability regions.

20: Our technique is a combination of static analysis to estimate quantization 

21: errors for specific controller implementations

22: and stochastic local search over the space of possible controllers using particle swarm optimization.

23: The effectiveness of our technique is illustrated using examples of

24: various standard control systems: 

25: in most examples, we achieve controllers with close

26: LQR-LQG performance but with implementation errors, hence regions of practical stability, 

27: several times as small.

28: \end{abstract}

29: