1 Introduction
2 Related work
2.1 CEGIS
2.2 Discretization effects in control design
3 Preliminaries
3.1 State-space representation of physical systems
3.2 Digital control synthesis
3.3 Stability of closed-loop models
3.4 Safety of closed-loop models
3.5 Bounded model checking
3.6 Semantics of finite-precision arithmetic
- The ADC converts the analog signal x(t) into a digital signal \(x_k\), which is then fed into the controller, converting a real value to a finite-precision value.
- The controller block performs arithmetic at finite precision. We assume the ADC represents numbers with at least the same precision as the controller, and thus focus on the precision as limited by the controller. This is a reasonable assumption based on commonly available hardware.
- The DAC converts finite-precision values back to real values. We assume that the input to the DAC has the same precision as the output of the controller. It would, however, be straightforward to account for a DAC or ADC of different precision than the controller in our algorithm, if necessary.
3.7 Soundness of modelling
- We account for the error introduced by finite-precision arithmetic applied over the model variables \(x_k\) and \(u_k\), which are actually continuous quantities. We guarantee that the precision we use to represent the model variables is at least as precise as the precision used in the digital controller, and we use interval arithmetic to bound the incurred errors, as further detailed in Sect. 5.
3.8 Notation for fixed- and floating-point precision
3.9 Counterexample-guided inductive synthesis (CEGIS)
4 Formal specification of stability on a model
4.1 Jury’s stability criterion
5 Numerical representation and soundness
5.1 Bit-precise bounded model checking
5.2 Interval arithmetic for errors in numerical representations
5.3 Effect of finite-precision arithmetic on safety specification and on stability
5.3.1 Safety of closed-loop models with finite-precision controller error
5.3.2 Stability of closed-loop models with fixed-point controller error
6 Synthesis of digital controllers with CEGIS
6.1 synthesize block
6.2 safety block
6.3 precision block
6.4 complete block
7 DSSynth: a software tool for automated digital controller synthesis over physical plants
nondet
, CPROVER_assume
intrinsic functions).8 Experimental evaluation
8.1 Description of the control benchmarks
8.2 Objectives
- Show that the multi-staged CEGIS approach is able to generate finite-precision digital controllers using fixed-point and floating-point arithmetic in a reasonable amount of time.
8.3 Results
Benchmark | Order | \({\mathcal {F}}_{\langle I_p,F_p \rangle }\) | Time (s) | k | \({\mathcal {F}}_{\langle E_p, M_p \rangle }\) | Time (s) | k |
---|---|---|---|---|---|---|---|
Bioreact | 2 | 8,8 | 15.35 | 4 | 10,6 | 23.76 | 2 |
Chen | 3 | 8,8 | 11.24 | 0 | 10,6 | 14.25 | 0 |
Cruise | 1 | 8,8 | 11.03 | 0 | 10,6 | 11.17 | 0 |
Cruise 2 | 1 | 8,8 | 9.93 | 0 | 10,6 | 10.54 | 0 |
Cst | 3 | 12,12 | 90.03 | 2 | 10,6 | 321.12 | 2 |
Cstrtmp | 2 | 8,8 | 18.56 | 2 | 10,6 | 16.99 | 2 |
DC motor | 2 | 8,8 | 10.34 | 0 | 10,6 | 12.32 | 0 |
Helicopter | 3 | 16,16 | 1116.08 | 2 | 10,6 | 168.43 | 38 |
Inverted pendulum | 2 | 12,12 | 16.01 | 2 | 10,6 | 18.73 | 0 |
Magnetic pointer | 3 | 12,12 | 1071.02 | 10 | 10,6 | 207.60 | 9 |
Magnetic suspension | 3 | 20,20 | 56.9 | 2 | 10,6 | 998.3 | 6 |
Pendulum | 2 | 8,8 | 11.74 | 0 | 10,6 | 13.69 | 0 |
Regulator | 5 | ✗ | 10,16 | 190.28 | 2 | ||
Satellite | 2 | 8,8 | 13.91 | 3 | 10,6 | 16.92 | 7 |
Spring-mass-damper | 2 | 12,12 | 16.09 | 0 | 10,6 | 23.21 | 4 |
Steam drum | 3 | ✗ | 10,16 | 21.16 | 4 | ||
Supension | 4 | 8,8 | 12.40 | 5 | 10,6 | 17.03 | 5 |
Tape driver | 3 | 8,8 | 12.18 | 0 | 10,6 | 14.34 | 0 |
USCG tampa | 3 | 12,12 | 1143.35 | 10 | 10,6 | 210.70 | 9 |
8.4 Threats to generality
- Benchmark selection: We report an assessment of both our approaches over a diverse set of real-world benchmarks. Nevertheless, this set of benchmarks is limited within the scope of this paper and the performance may not generalize to other benchmarks.
- Plant model precision and discretization heuristics: Our algorithm to select suitable finite-precision arithmetic to model the plant behavior increases the precision by 8 bits at each step, in order to be compliant with the CBMC type API. Similarly, for time-discretization, we try a set of pre-defined time discretisations. This works sufficiently well for our benchmarks, but performance may suffer in some cases, for example if the completeness threshold is high.