File preview
Teaching CPS Foundations With Contracts
Andr´ Platzer e
aplatzer@cs.cmu.edu Computer Science Department Carnegie Mellon University, Pittsburgh, PA
http://symbolaris.com/course/fcps13.html
0.5 0.4 0.3 0.2 0.1
1.0
0.8
0.6
0.4
0.2
Andr´ Platzer (CMU) e
Teaching CPS Foundations With Contracts
CPS-Ed
1/8
Can you trust a computer to control physics?
Andr´ Platzer (CMU) e
Teaching CPS Foundations With Contracts
CPS-Ed
2/8
CPS Analysis & Design: Robot Lab
Challenge (Hybrid Systems)
Design & verify controller for a robot avoiding obstacles Accelerate / brake (discrete dynamics) 1D motion (continuous dynamics)
a
0.2 0.8 0.1 2.0 2 0.1 0.2 0.3 2 4 6 8 10 4 6 8 10 2.5
3.5 3.0 2.5 2.0 1.5 1.0 0.5 0.0 0 1 2 3 4 5 6
v
p
px
t0.6
0.4 0.2
1.5 1.0 0.5
py
t
2
4
6
8
10
t
Andr´ Platzer (CMU) e
Teaching CPS Foundations With Contracts
CPS-Ed
3/8
CPS Analysis & Design: Robot Lab
Challenge (Hybrid Systems)
Design & verify controller for a robot avoiding obstacles Accelerate / brake (discrete dynamics) 1D motion (continuous dynamics)
a
0.2 0.00008 0.1 0.8 0.00006 0.6 0.00004 0.1 0.00002 0.2 0.3 2 4 6 8 10 0.2 0.4
3.5 3.0 2.5 2.0 1.5 1.0 0.5 0.0 0 1 2 3 4 5 6
Ω
d
1.0
dx
2
4
6
8
10
t
t
2 4
dy
6
8
10
t
Andr´ Platzer (CMU) e
Teaching CPS Foundations With Contracts
CPS-Ed
3/8
CPS Analysis & Design: Robot Lab
Challenge (Hybrid Systems)
Design & verify controller for a robot avoiding obstacles Accel / brake / steer (discrete dynamics) 2D motion (continuous dynamics)
a
0.2 2 0.2 0.4 0.6 0.8 2 4 6 8 4 6 8 10
3.5 3.0 2.5 2.0 1.5 1.0 0.5 0.0 0 1 2 3 4 5 6
v
1.0
p
8
t
0.8 6 0.6
px
0.4 0.2 10 t 4 2
py
2 4 6 8 10
t
Andr´ Platzer (CMU) e
Teaching CPS Foundations With Contracts
CPS-Ed
4/8
CPS Analysis & Design: Robot Lab
Challenge (Hybrid Systems)
Design & verify controller for a robot avoiding obstacles Accel / brake / steer (discrete dynamics) 2D motion (continuous dynamics)
a
0.2 2 0.2 0.4 0.6 0.8 0.5 2 1.0 0.5 4 4 6 8 10 t 2 4 6 8 10
3.5 3.0 2.5 2.0 1.5 1.0 0.5 0.0 0 1 2 3 4 5 6
Ω
0.5
d
1.0
dx
t
0.5
dy
6
8
10
t
Andr´ Platzer (CMU) e
Teaching CPS Foundations With Contracts
CPS-Ed
4/8
CPS Analysis & Design: Robot Lab
Challenge (Hybrid Systems)
Design & verify controller for a robot avoiding obstacles Dynamic obstacles (other agents) Avoid collisions (define safety)
a
2 1 4 6 8 10
3.5 3.0 2.5 2.0 1.5 1.0 0.5 0.0 0 1 2 3 4 5 6
v t1.0
0.8 0.6
p
4
px
3 2 0.4 3 0.2 4 2 4 6 8 10 t
2
1
py
2 4 6 8 10
t
Andr´ Platzer (CMU) e
Teaching CPS Foundations With Contracts
CPS-Ed
5/8
CPS Analysis & Design: Robot Lab
Challenge (Hybrid Systems)
Design & verify controller for a robot avoiding obstacles Dynamic obstacles (other agents) Avoid collisions (define safety)
a
2 1 0.5 2 0.5 3 1.0 4 0.5 2 4 6 8 10 4 6 8 10
3.5 3.0 2.5 2.0 1.5 1.0 0.5 0.0 0 1 2 3 4 5 6
Ω t
0.5
d
1.0
dx
t
2 4 6 8 10
t
dy
Andr´ Platzer (CMU) e
Teaching CPS Foundations With Contracts
CPS-Ed
5/8
CPS Analysis & Design: Robot Lab
Challenge (Hybrid Systems)
Design & verify controller for a robot avoiding obstacles Control robot (respect delays) Environment interaction (obstacles, agents, uncertainty)
a
0.4 1.0 0.2 2 0.2 0.4 0.4 0.2 0.6 2 4 6 8 10 2 1 4 6 8 10 6 5 4 0.6 3
3.5 3.0 2.5 2.0 1.5 1.0 0.5 0.0 0 1 2 3 4 5 6
v
1.2
p
7
t
0.8
px
t
2 4
py
6 8 10
t
Andr´ Platzer (CMU) e
Teaching CPS Foundations With Contracts
CPS-Ed
6/8
CPS Analysis & Design: Robot Lab
Challenge (Hybrid Systems)
Design & verify controller for a robot avoiding obstacles Control robot (respect delays) Environment interaction (obstacles, agents, uncertainty)
a
0.4 0.5 0.2 2 0.2 0.4 1.0 0.6 0.5 4 6 8 10 0.5
3.5 3.0 2.5 2.0 1.5 1.0 0.5 0.0 0 1 2 3 4 5 6
Ω
d
1.0
dx dy
2 4 6 8 10
t
0.5
2
4
6
8
10
t
t
Andr´ Platzer (CMU) e
Teaching CPS Foundations With Contracts
CPS-Ed
6/8
CPS Design & CPS Contracts in Programs
HP Reveal in layers Contracts Reason about CPS
@ r e q u i r e s ( v ˆ2 <= 2∗ b ∗ (m ) ) −x @ r e q u i r e s ( v>=0 & A>=0 & b>0) @ensures ( x<= m) { i f ( v ˆ2 <= 2∗ b ∗ (m ) − (A+b ) ∗ (A+2∗v ) ) { −x a := A ; } else { a := −b ; } t := 0 ; {x ’=v , v ’=a , t ’=1 , v>=0 & t <=1} }∗ @ i n v a r i a n t ( v ˆ2 <= 2∗ b ∗ (m ) ) −x CPS Simulate for intuition CT Design-by-invariant
CPS-Ed 7/8
Andr´ Platzer (CMU) e
Teaching CPS Foundations With Contracts
Teaching CPS Foundations With Contracts
differential dynamic logic
dL = DL + HP
d i s cr
e te
c o n ti n
[α]φ
Ω
0.5
α
d
1.0
φ
uous
dx dy
2 4 6 8 10
2 0.5 1.0
4
6
8
10
t
0.5
t
0.5
al
stoc
nondet
Develop CPS models Express CPS contracts Intuition for operation
rsar i
adv e
KeYmaera
has tic
Reason rigorously about CPS Focus on core principles CPS programs + contracts
Andr´ Platzer (CMU) e Teaching CPS Foundations With Contracts CPS-Ed 8/8
pre / postconditions
design-byinvariant
abstraction & architectures
rigorous reasoning
Computational Thinking
specs & properties verification
CPS Foundations Learning Objectives
modelpredictive control
core principles
CPS skills
Modeling & Control
develop
operational effects dynamical aspects
semantics
Andr´ Platzer (CMU) e
Teaching CPS Foundations With Contracts
CPS-Ed
1/4
Successful Hybrid Systems Proofs
0 *
far neg
4 [d := *] 3 [m := *]
[SB := ((amax / b + 1) * ep * v + (v ^ 2 - d ^ 2) / (2 * b) + ((amax / b + 1) * amax * ep ^ 2) / 2)] 1 [do := d] 2 [state := brake] [?v <= vdes] 10 [?v >= vdes] 13
[mo := m]
8
[a := *]
[a := *]
11
14
[?a >= 0 & a <= amax] [?a <= 0 & a >= -b] 12 15
cor fsa
y
5 [vdes := *] 6
24 [?m - z <= SB | state = brake] [?m - z >= SB & state != brake] 17 *
[?d >= 0 & do ^ 2 - d ^ 2 <= 2 * b * (m - mo) & vdes >= 0]
[a := -b]
19
7
18
17
28 [t := 0]
rec
21 [{z‘ = v, v‘ = a, t‘ = 1, v >= 0 & t <= ep}] 22
31
y2 x2 x1
Andr´ Platzer (CMU) e
x
c
it ex
c x
¯ ϑ ̟
c
entry
y
z y c
x
ω e d
y1
x
Teaching CPS Foundations With Contracts CPS-Ed 2/4
Successful Hybrid Systems Proofs
(rx , ry ) fy (vx , vy ) ey (lx , ly ) xb ex fx
Andr´ Platzer (CMU) e
Teaching CPS Foundations With Contracts
CPS-Ed
2/4
Successful Hybrid Systems Proofs
z y c x
Virtual fixture boundary
xi di
xl
m i inr
2
nr mi
i
disc i
xi
x j p
xk xm
D
d
0.3 0.3 0.2 0.1 0.1 0.2 0.3 5 10 15 20 0.1 0.2
1 0.2 0.4 0.6 0.8 1.0
0.2 0.1 0.0
-1
Andr´ Platzer (CMU) e
Teaching CPS Foundations With Contracts 0.3
CPS-Ed
2/4
Logic for Hybrid Systems
differential dynamic logic
dL = FOLR v
v 2 ≤ 2b(M − z) z M
Andr´ Platzer (CMU) e
Teaching CPS Foundations With Contracts
CPS-Ed
3/4
Logic for Hybrid Systems
differential dynamic logic
dL = FOLR + DL + HP v 2 ≤ 2b C → [ if(z > SB) a := −b; z =
hybrid program
a ] v2
≤ 2b
v 2 ≤ 2b v 2 ≤ 2b
Andr´ Platzer (CMU) e
Teaching CPS Foundations With Contracts
CPS-Ed
3/4
Logic for Hybrid Systems
differential dynamic logic
dL = FOLR + DL + HP v 2 ≤ 2b C → [ if(z > SB) a := −b; z =
hybrid program
a ] v2
≤ 2b
v 2 ≤ 2b v 2 ≤ 2b
Initial condition
System dynamics
Post condition
Andr´ Platzer (CMU) e
Teaching CPS Foundations With Contracts
CPS-Ed
3/4
Differential Dynamic Logic: Axiomatization
[:=] [?] [] [∪] [;] [∗ ] K I C [x := θ][(x)]φx ↔ [(x)]φθ [?H]φ ↔ (H → φ) [x = f (x)]φ ↔ ∀t≥0 [x := y (t)]φ [α ∪ β]φ ↔ [α]φ ∧ [β]φ [α; β]φ ↔ [α][β]φ [α∗ ]φ ↔ φ ∧ [α][α∗ ]φ [α](φ → ψ) → ([α]φ → [α]ψ) [α∗ ](φ → [α]φ) → (φ → [α∗ ]φ) [α∗ ]∀v >0 (ϕ(v ) → α ϕ(v − 1)) → ∀v (ϕ(v ) → α∗ ∃v ≤0 ϕ(v ))
Teaching CPS Foundations With Contracts CPS-Ed 4/4
(y (t) = f (y ))
Andr´ Platzer (CMU) e
Andr´ Platzer. e Differential dynamic logic for hybrid systems. J. Autom. Reas., 41(2):143–189, 2008. Andr´ Platzer. e Logical Analysis of Hybrid Systems: Proving Theorems for Complex Dynamics. Springer, Heidelberg, 2010. Andr´ Platzer. e Logics of dynamical systems. In LICS, pages 13–24. IEEE, 2012. Andr´ Platzer and Jan-David Quesel. e KeYmaera: A hybrid theorem prover for hybrid systems. In Alessandro Armando, Peter Baumgartner, and Gilles Dowek, editors, IJCAR, volume 5195 of LNCS, pages 171–178. Springer, 2008.
Andr´ Platzer (CMU) e
Teaching CPS Foundations With Contracts
CPS-Ed
4/4
Andr´ Platzer e
aplatzer@cs.cmu.edu Computer Science Department Carnegie Mellon University, Pittsburgh, PA
http://symbolaris.com/course/fcps13.html
0.5 0.4 0.3 0.2 0.1
1.0
0.8
0.6
0.4
0.2
Andr´ Platzer (CMU) e
Teaching CPS Foundations With Contracts
CPS-Ed
1/8
Can you trust a computer to control physics?
Andr´ Platzer (CMU) e
Teaching CPS Foundations With Contracts
CPS-Ed
2/8
CPS Analysis & Design: Robot Lab
Challenge (Hybrid Systems)
Design & verify controller for a robot avoiding obstacles Accelerate / brake (discrete dynamics) 1D motion (continuous dynamics)
a
0.2 0.8 0.1 2.0 2 0.1 0.2 0.3 2 4 6 8 10 4 6 8 10 2.5
3.5 3.0 2.5 2.0 1.5 1.0 0.5 0.0 0 1 2 3 4 5 6
v
p
px
t0.6
0.4 0.2
1.5 1.0 0.5
py
t
2
4
6
8
10
t
Andr´ Platzer (CMU) e
Teaching CPS Foundations With Contracts
CPS-Ed
3/8
CPS Analysis & Design: Robot Lab
Challenge (Hybrid Systems)
Design & verify controller for a robot avoiding obstacles Accelerate / brake (discrete dynamics) 1D motion (continuous dynamics)
a
0.2 0.00008 0.1 0.8 0.00006 0.6 0.00004 0.1 0.00002 0.2 0.3 2 4 6 8 10 0.2 0.4
3.5 3.0 2.5 2.0 1.5 1.0 0.5 0.0 0 1 2 3 4 5 6
Ω
d
1.0
dx
2
4
6
8
10
t
t
2 4
dy
6
8
10
t
Andr´ Platzer (CMU) e
Teaching CPS Foundations With Contracts
CPS-Ed
3/8
CPS Analysis & Design: Robot Lab
Challenge (Hybrid Systems)
Design & verify controller for a robot avoiding obstacles Accel / brake / steer (discrete dynamics) 2D motion (continuous dynamics)
a
0.2 2 0.2 0.4 0.6 0.8 2 4 6 8 4 6 8 10
3.5 3.0 2.5 2.0 1.5 1.0 0.5 0.0 0 1 2 3 4 5 6
v
1.0
p
8
t
0.8 6 0.6
px
0.4 0.2 10 t 4 2
py
2 4 6 8 10
t
Andr´ Platzer (CMU) e
Teaching CPS Foundations With Contracts
CPS-Ed
4/8
CPS Analysis & Design: Robot Lab
Challenge (Hybrid Systems)
Design & verify controller for a robot avoiding obstacles Accel / brake / steer (discrete dynamics) 2D motion (continuous dynamics)
a
0.2 2 0.2 0.4 0.6 0.8 0.5 2 1.0 0.5 4 4 6 8 10 t 2 4 6 8 10
3.5 3.0 2.5 2.0 1.5 1.0 0.5 0.0 0 1 2 3 4 5 6
Ω
0.5
d
1.0
dx
t
0.5
dy
6
8
10
t
Andr´ Platzer (CMU) e
Teaching CPS Foundations With Contracts
CPS-Ed
4/8
CPS Analysis & Design: Robot Lab
Challenge (Hybrid Systems)
Design & verify controller for a robot avoiding obstacles Dynamic obstacles (other agents) Avoid collisions (define safety)
a
2 1 4 6 8 10
3.5 3.0 2.5 2.0 1.5 1.0 0.5 0.0 0 1 2 3 4 5 6
v t1.0
0.8 0.6
p
4
px
3 2 0.4 3 0.2 4 2 4 6 8 10 t
2
1
py
2 4 6 8 10
t
Andr´ Platzer (CMU) e
Teaching CPS Foundations With Contracts
CPS-Ed
5/8
CPS Analysis & Design: Robot Lab
Challenge (Hybrid Systems)
Design & verify controller for a robot avoiding obstacles Dynamic obstacles (other agents) Avoid collisions (define safety)
a
2 1 0.5 2 0.5 3 1.0 4 0.5 2 4 6 8 10 4 6 8 10
3.5 3.0 2.5 2.0 1.5 1.0 0.5 0.0 0 1 2 3 4 5 6
Ω t
0.5
d
1.0
dx
t
2 4 6 8 10
t
dy
Andr´ Platzer (CMU) e
Teaching CPS Foundations With Contracts
CPS-Ed
5/8
CPS Analysis & Design: Robot Lab
Challenge (Hybrid Systems)
Design & verify controller for a robot avoiding obstacles Control robot (respect delays) Environment interaction (obstacles, agents, uncertainty)
a
0.4 1.0 0.2 2 0.2 0.4 0.4 0.2 0.6 2 4 6 8 10 2 1 4 6 8 10 6 5 4 0.6 3
3.5 3.0 2.5 2.0 1.5 1.0 0.5 0.0 0 1 2 3 4 5 6
v
1.2
p
7
t
0.8
px
t
2 4
py
6 8 10
t
Andr´ Platzer (CMU) e
Teaching CPS Foundations With Contracts
CPS-Ed
6/8
CPS Analysis & Design: Robot Lab
Challenge (Hybrid Systems)
Design & verify controller for a robot avoiding obstacles Control robot (respect delays) Environment interaction (obstacles, agents, uncertainty)
a
0.4 0.5 0.2 2 0.2 0.4 1.0 0.6 0.5 4 6 8 10 0.5
3.5 3.0 2.5 2.0 1.5 1.0 0.5 0.0 0 1 2 3 4 5 6
Ω
d
1.0
dx dy
2 4 6 8 10
t
0.5
2
4
6
8
10
t
t
Andr´ Platzer (CMU) e
Teaching CPS Foundations With Contracts
CPS-Ed
6/8
CPS Design & CPS Contracts in Programs
HP Reveal in layers Contracts Reason about CPS
@ r e q u i r e s ( v ˆ2 <= 2∗ b ∗ (m ) ) −x @ r e q u i r e s ( v>=0 & A>=0 & b>0) @ensures ( x<= m) { i f ( v ˆ2 <= 2∗ b ∗ (m ) − (A+b ) ∗ (A+2∗v ) ) { −x a := A ; } else { a := −b ; } t := 0 ; {x ’=v , v ’=a , t ’=1 , v>=0 & t <=1} }∗ @ i n v a r i a n t ( v ˆ2 <= 2∗ b ∗ (m ) ) −x CPS Simulate for intuition CT Design-by-invariant
CPS-Ed 7/8
Andr´ Platzer (CMU) e
Teaching CPS Foundations With Contracts
Teaching CPS Foundations With Contracts
differential dynamic logic
dL = DL + HP
d i s cr
e te
c o n ti n
[α]φ
Ω
0.5
α
d
1.0
φ
uous
dx dy
2 4 6 8 10
2 0.5 1.0
4
6
8
10
t
0.5
t
0.5
al
stoc
nondet
Develop CPS models Express CPS contracts Intuition for operation
rsar i
adv e
KeYmaera
has tic
Reason rigorously about CPS Focus on core principles CPS programs + contracts
Andr´ Platzer (CMU) e Teaching CPS Foundations With Contracts CPS-Ed 8/8
pre / postconditions
design-byinvariant
abstraction & architectures
rigorous reasoning
Computational Thinking
specs & properties verification
CPS Foundations Learning Objectives
modelpredictive control
core principles
CPS skills
Modeling & Control
develop
operational effects dynamical aspects
semantics
Andr´ Platzer (CMU) e
Teaching CPS Foundations With Contracts
CPS-Ed
1/4
Successful Hybrid Systems Proofs
0 *
far neg
4 [d := *] 3 [m := *]
[SB := ((amax / b + 1) * ep * v + (v ^ 2 - d ^ 2) / (2 * b) + ((amax / b + 1) * amax * ep ^ 2) / 2)] 1 [do := d] 2 [state := brake] [?v <= vdes] 10 [?v >= vdes] 13
[mo := m]
8
[a := *]
[a := *]
11
14
[?a >= 0 & a <= amax] [?a <= 0 & a >= -b] 12 15
cor fsa
y
5 [vdes := *] 6
24 [?m - z <= SB | state = brake] [?m - z >= SB & state != brake] 17 *
[?d >= 0 & do ^ 2 - d ^ 2 <= 2 * b * (m - mo) & vdes >= 0]
[a := -b]
19
7
18
17
28 [t := 0]
rec
21 [{z‘ = v, v‘ = a, t‘ = 1, v >= 0 & t <= ep}] 22
31
y2 x2 x1
Andr´ Platzer (CMU) e
x
c
it ex
c x
¯ ϑ ̟
c
entry
y
z y c
x
ω e d
y1
x
Teaching CPS Foundations With Contracts CPS-Ed 2/4
Successful Hybrid Systems Proofs
(rx , ry ) fy (vx , vy ) ey (lx , ly ) xb ex fx
Andr´ Platzer (CMU) e
Teaching CPS Foundations With Contracts
CPS-Ed
2/4
Successful Hybrid Systems Proofs
z y c x
Virtual fixture boundary
xi di
xl
m i inr
2
nr mi
i
disc i
xi
x j p
xk xm
D
d
0.3 0.3 0.2 0.1 0.1 0.2 0.3 5 10 15 20 0.1 0.2
1 0.2 0.4 0.6 0.8 1.0
0.2 0.1 0.0
-1
Andr´ Platzer (CMU) e
Teaching CPS Foundations With Contracts 0.3
CPS-Ed
2/4
Logic for Hybrid Systems
differential dynamic logic
dL = FOLR v
v 2 ≤ 2b(M − z) z M
Andr´ Platzer (CMU) e
Teaching CPS Foundations With Contracts
CPS-Ed
3/4
Logic for Hybrid Systems
differential dynamic logic
dL = FOLR + DL + HP v 2 ≤ 2b C → [ if(z > SB) a := −b; z =
hybrid program
a ] v2
≤ 2b
v 2 ≤ 2b v 2 ≤ 2b
Andr´ Platzer (CMU) e
Teaching CPS Foundations With Contracts
CPS-Ed
3/4
Logic for Hybrid Systems
differential dynamic logic
dL = FOLR + DL + HP v 2 ≤ 2b C → [ if(z > SB) a := −b; z =
hybrid program
a ] v2
≤ 2b
v 2 ≤ 2b v 2 ≤ 2b
Initial condition
System dynamics
Post condition
Andr´ Platzer (CMU) e
Teaching CPS Foundations With Contracts
CPS-Ed
3/4
Differential Dynamic Logic: Axiomatization
[:=] [?] [] [∪] [;] [∗ ] K I C [x := θ][(x)]φx ↔ [(x)]φθ [?H]φ ↔ (H → φ) [x = f (x)]φ ↔ ∀t≥0 [x := y (t)]φ [α ∪ β]φ ↔ [α]φ ∧ [β]φ [α; β]φ ↔ [α][β]φ [α∗ ]φ ↔ φ ∧ [α][α∗ ]φ [α](φ → ψ) → ([α]φ → [α]ψ) [α∗ ](φ → [α]φ) → (φ → [α∗ ]φ) [α∗ ]∀v >0 (ϕ(v ) → α ϕ(v − 1)) → ∀v (ϕ(v ) → α∗ ∃v ≤0 ϕ(v ))
Teaching CPS Foundations With Contracts CPS-Ed 4/4
(y (t) = f (y ))
Andr´ Platzer (CMU) e
Andr´ Platzer. e Differential dynamic logic for hybrid systems. J. Autom. Reas., 41(2):143–189, 2008. Andr´ Platzer. e Logical Analysis of Hybrid Systems: Proving Theorems for Complex Dynamics. Springer, Heidelberg, 2010. Andr´ Platzer. e Logics of dynamical systems. In LICS, pages 13–24. IEEE, 2012. Andr´ Platzer and Jan-David Quesel. e KeYmaera: A hybrid theorem prover for hybrid systems. In Alessandro Armando, Peter Baumgartner, and Gilles Dowek, editors, IJCAR, volume 5195 of LNCS, pages 171–178. Springer, 2008.
Andr´ Platzer (CMU) e
Teaching CPS Foundations With Contracts
CPS-Ed
4/4