File preview
Teaching CPS Foundations With Contracts
André Platzer
Lab 1
3.5
Design & verify controller for a robot avoiding obstacles - Accelerate / brake
(discrete dynamics)
Computer Science Department Carnegie Mellon University
3.0 2.5 2.0 1. 1.5 1. 1.0 0. 0.5 0.0
- 1D motion
(continuous dynamics)
a
0.2 0.1
0
1
2
3
4
5
6
d
1.0
p
dx
2.5 2.0
ω
px
0.00008 0.00006
v
0.8 0.6 0.4 0.2
0.8
pre-/post condition
6 8 10
rigorous reasoning
2 - 0.1 - 0.2 - 0.3
4
6
8
10
t
0.6 1.5 0.4 0.2 1.0 0.5 2 4
py
0.00004 0.00002
dy
6
8
10
t
2
4
6
8
10
t
2
4
6
8
10
t
2
4
t
Lab 2
3.5
Design & verify controller for a robot avoiding obstacles - Accel / brake / steer
(discrete dynamics)
3.0 2.5 2.0 1. 1.5 1. 1.0 0. 0.5 0.0
operational effects
core principles
- 2D motion
(continuous dynamics)
a
0.2 0.8 2 - 0.2 - 0.4 - 0.6 - 0.8 0.4 0.2 10 t 4 4 6 8 10
0
1
2
3
4
5
6
v
1.0
p
8
ω
0.5
d
1.0
t
dx
HP
Reveal in layers
Contracts
Reason about CPS
6 0.6
px
2 - 0.5 2 4 6 8 10
t
0.5
2
4
py
2 4 6 8
dy
6
8
10
t
2
4
6
8
10 t
- 1.0 - 0.5
Lab 3
3.5
Design & verify controller for a robot avoiding obstacles - Dynamic obstacles
(other agents)
3.0 2.5 2.0 1.5 1.0 0.5 0.0
@ 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− x ) − (A+b ) * (A+2 * v ) ) { 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
- Avoid collisions
(de ne safety)
a
2 - 1 4 6 8 10 t
0
1
2
3
4
5
6
v
1.0 0.8
p
4
px
ω
0.5 10 t
d
1.0
3 0.6
dx
- 2 0.4 - 3 0.2
0.5
2
2
4
6
8
1
py
2 4 6 8 10 t
- 0.5
2
4
6
8
10
t
- 4
2
4
6
8
10
t
dy
- 1.0 - 0.5
di erential dynamic logic
Lab 4
3.5
dL = FOL R + DL + HP v 2 ≤ 2b C [ if ( z > SB ) a := − b; z“ = a ] v 2 ≤ 2b
hybrid program
1. 1.5 1. 1.0 0. 0.5 0.0
Design & verify controller for a robot avoiding obstacles - Control robot
(respect delays)
3.0 2.5 2.0
v 2 ≤ 2b v 2 ≤ 2b
- Environment interaction
(obstacles, agents, uncertainty)
a
0.4 0.2 2 - 0.2 - 0.4 - 0.6 4 6 8 10
Initial condition
0 1 2 3 4 5 6
System dynamics
Post condition
v
1.2 1.0 0.8
p
7 6 5 0.5 4 3 2
ω
px
2 - 0.5 4 6 8 10 t
d
1.0
dx dy
2 4 6 8 10
t
0.6 0.4 0.2 2 4 6 8 10
0.5
t
1 2 4
t
py
6 8 10
t
- 1.0 - 0.5
http://symbolaris.com/course/fcps13.html
André Platzer
Lab 1
3.5
Design & verify controller for a robot avoiding obstacles - Accelerate / brake
(discrete dynamics)
Computer Science Department Carnegie Mellon University
3.0 2.5 2.0 1. 1.5 1. 1.0 0. 0.5 0.0
- 1D motion
(continuous dynamics)
a
0.2 0.1
0
1
2
3
4
5
6
d
1.0
p
dx
2.5 2.0
ω
px
0.00008 0.00006
v
0.8 0.6 0.4 0.2
0.8
pre-/post condition
6 8 10
rigorous reasoning
2 - 0.1 - 0.2 - 0.3
4
6
8
10
t
0.6 1.5 0.4 0.2 1.0 0.5 2 4
py
0.00004 0.00002
dy
6
8
10
t
2
4
6
8
10
t
2
4
6
8
10
t
2
4
t
Lab 2
3.5
Design & verify controller for a robot avoiding obstacles - Accel / brake / steer
(discrete dynamics)
3.0 2.5 2.0 1. 1.5 1. 1.0 0. 0.5 0.0
operational effects
core principles
- 2D motion
(continuous dynamics)
a
0.2 0.8 2 - 0.2 - 0.4 - 0.6 - 0.8 0.4 0.2 10 t 4 4 6 8 10
0
1
2
3
4
5
6
v
1.0
p
8
ω
0.5
d
1.0
t
dx
HP
Reveal in layers
Contracts
Reason about CPS
6 0.6
px
2 - 0.5 2 4 6 8 10
t
0.5
2
4
py
2 4 6 8
dy
6
8
10
t
2
4
6
8
10 t
- 1.0 - 0.5
Lab 3
3.5
Design & verify controller for a robot avoiding obstacles - Dynamic obstacles
(other agents)
3.0 2.5 2.0 1.5 1.0 0.5 0.0
@ 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− x ) − (A+b ) * (A+2 * v ) ) { 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
- Avoid collisions
(de ne safety)
a
2 - 1 4 6 8 10 t
0
1
2
3
4
5
6
v
1.0 0.8
p
4
px
ω
0.5 10 t
d
1.0
3 0.6
dx
- 2 0.4 - 3 0.2
0.5
2
2
4
6
8
1
py
2 4 6 8 10 t
- 0.5
2
4
6
8
10
t
- 4
2
4
6
8
10
t
dy
- 1.0 - 0.5
di erential dynamic logic
Lab 4
3.5
dL = FOL R + DL + HP v 2 ≤ 2b C [ if ( z > SB ) a := − b; z“ = a ] v 2 ≤ 2b
hybrid program
1. 1.5 1. 1.0 0. 0.5 0.0
Design & verify controller for a robot avoiding obstacles - Control robot
(respect delays)
3.0 2.5 2.0
v 2 ≤ 2b v 2 ≤ 2b
- Environment interaction
(obstacles, agents, uncertainty)
a
0.4 0.2 2 - 0.2 - 0.4 - 0.6 4 6 8 10
Initial condition
0 1 2 3 4 5 6
System dynamics
Post condition
v
1.2 1.0 0.8
p
7 6 5 0.5 4 3 2
ω
px
2 - 0.5 4 6 8 10 t
d
1.0
dx dy
2 4 6 8 10
t
0.6 0.4 0.2 2 4 6 8 10
0.5
t
1 2 4
t
py
6 8 10
t
- 1.0 - 0.5
http://symbolaris.com/course/fcps13.html