Presentation

Delayed Nondeterminism in
Model Checking Embedded Systems Assembly Code
Thomas Noll1
Bastian Schlich2
1 Software
Modelling and Verification Group
for Embedded Systems
RWTH Aachen University
[email protected]
2 Software
Haifa Verification Conference, October 25, 2007
C Code vs. Assembly Code
Most microcontroller software written in C
Many model checkers accept (ANSI) C programs: BLAST, CBMC,
MAGIC, ...
Often restricted support of C constructs:
no expressions with side effects
no recursion
only integer variables
...
Many microcontroller features not considered in ANSI C:
direct hardware access (registers, ...)
embedded assembly code
interrupts
...
Case studies from industrial applications contain errors which
passed all tests and reviews
are only observable on assembly level
caused by forgotten interrupt enabling/disabling, reentrance problems, ...
=⇒ Base model checking on assembly code
Delayed Nondeterminism
HVC 2007
2
C Code vs. Assembly Code
Most microcontroller software written in C
Many model checkers accept (ANSI) C programs: BLAST, CBMC,
MAGIC, ...
Often restricted support of C constructs:
no expressions with side effects
no recursion
only integer variables
...
Many microcontroller features not considered in ANSI C:
direct hardware access (registers, ...)
embedded assembly code
interrupts
...
Case studies from industrial applications contain errors which
passed all tests and reviews
are only observable on assembly level
caused by forgotten interrupt enabling/disabling, reentrance problems, ...
=⇒ Base model checking on assembly code
Delayed Nondeterminism
HVC 2007
2
C Code vs. Assembly Code
Most microcontroller software written in C
Many model checkers accept (ANSI) C programs: BLAST, CBMC,
MAGIC, ...
Often restricted support of C constructs:
no expressions with side effects
no recursion
only integer variables
...
Many microcontroller features not considered in ANSI C:
direct hardware access (registers, ...)
embedded assembly code
interrupts
...
Case studies from industrial applications contain errors which
passed all tests and reviews
are only observable on assembly level
caused by forgotten interrupt enabling/disabling, reentrance problems, ...
=⇒ Base model checking on assembly code
Delayed Nondeterminism
HVC 2007
2
C Code vs. Assembly Code
Most microcontroller software written in C
Many model checkers accept (ANSI) C programs: BLAST, CBMC,
MAGIC, ...
Often restricted support of C constructs:
no expressions with side effects
no recursion
only integer variables
...
Many microcontroller features not considered in ANSI C:
direct hardware access (registers, ...)
embedded assembly code
interrupts
...
Case studies from industrial applications contain errors which
passed all tests and reviews
are only observable on assembly level
caused by forgotten interrupt enabling/disabling, reentrance problems, ...
=⇒ Base model checking on assembly code
Delayed Nondeterminism
HVC 2007
2
C Code Before Preprocessing
int main (void) {
init();// call initialization
sei();
while(1) {
inputs = PINA & 0x0F;
cli();
if (direction < 5) {
if (inputs & (1 << 1)) {// down
if (direction = 2 || direction = 3) {
TCCR1B = 0x00;
TIFR = 0xFF;
TCNT1 = 0x00;
TIMSK = (1<<OCIE1A);
TCCR1B = 0x05;
direction = 1;
}
Delayed Nondeterminism
HVC 2007
4
C Code After Preprocessing
int main (void) {
init();
__asm__ __volatile__ ("sei" ::);
while(1) {
inputs = (*(volatile uint8_t *)((0x19) + 0x20)) & 0x0F;
asm__ __volatile__ ("cli" ::);
if (direction < 5) {
if (inputs & (1 << 1)) {
if (direction = 2 || direction = 3) {
(*(volatile uint8_t *)((0x2E) + 0x20)) = 0x00;
(*(volatile uint8_t *)((0x38) + 0x20)) = 0xFF;
(*(volatile uint16_t *)((0x2C) + 0x20)) = 0x00;
(*(volatile uint8_t *)((0x39) + 0x20)) = (1<<4);
(*(volatile uint8_t *)((0x2E) + 0x20)) = 0x05;
direction = 1;
}
Delayed Nondeterminism
HVC 2007
6
Pros and Cons of Using Assembly Code
Advantages:
Errors of all development stages detectable:
(C) programming errors
compiler errors
errors invisible in the C code (reentrance problems, ...)
errors in handling the hardware (interrupts, ...)
Instructions (relatively) easy to handle
Clean and well documented semantics
Implementation close to actual execution
Disadvantages:
Hardware dependency
=⇒ compiler-generating approach
Bigger state spaces (finer granularity)
=⇒ abstraction techniques
Delayed Nondeterminism
HVC 2007
7
Pros and Cons of Using Assembly Code
Advantages:
Errors of all development stages detectable:
(C) programming errors
compiler errors
errors invisible in the C code (reentrance problems, ...)
errors in handling the hardware (interrupts, ...)
Instructions (relatively) easy to handle
Clean and well documented semantics
Implementation close to actual execution
Disadvantages:
Hardware dependency
=⇒ compiler-generating approach
Bigger state spaces (finer granularity)
=⇒ abstraction techniques
Delayed Nondeterminism
HVC 2007
7
The [mc]square Model Checker
[mc]square
formula
parser
cfg
elf file
C file
preprocessor
formula
static analyzer
state space
assembly
program
simulator
model
checker
C file
graph
counterexample
generator
Delayed Nondeterminism
result
HVC 2007
8
The ATMEL ATmega16 Microcontroller
8-bit microcontroller
16 KB flash memory
1KByte internal SRAM
512 bytes EEPROM
3 timer/counter units
4 I/O Ports 8-bit
20 vectorized interrupts
Delayed Nondeterminism
HVC 2007
9
Sources of Nondeterminism
I/O ports
Timer
SPI
TWI
USART
...
Delayed Nondeterminism
HVC 2007
10
I/O Ports
Monitoring, access and control of I/O ports
via three special registers for each port:
Data Direction Register (DDR):
specifies input (= 0) or output (= 1)
property of corresponding pin
Basic means to monitor
and control external
hardware
Each 8 I/O pins
(byte access)
Port Register (PORT):
specifies values of output pins
Port Input Register (PIN):
contains values of input pins
(read-only)
Bidirectional
Delayed Nondeterminism
HVC 2007
11
I/O Ports
Monitoring, access and control of I/O ports
via three special registers for each port:
Data Direction Register (DDR):
specifies input (= 0) or output (= 1)
property of corresponding pin
Basic means to monitor
and control external
hardware
Each 8 I/O pins
(byte access)
Port Register (PORT):
specifies values of output pins
Port Input Register (PIN):
contains values of input pins
(read-only)
Bidirectional
Delayed Nondeterminism
HVC 2007
11
Impact on State Space I
DDRA:
0
0
0
0
0
0
0
0
...
IN R18 PINA
R18 = 0
R18 = 1
R18 = 2
Delayed Nondeterminism
...
R18 = 255
HVC 2007
12
Impact on State Space II
DDRA:
1
1
1
1
1
1
1
1
PORTA:
1
1
0
0
1
1
1
0
...
IN R18 PINA
R18 = 206
Delayed Nondeterminism
HVC 2007
13
Impact on State Space III
DDRA:
1
1
1
1
1
1
0
0
PORTA:
0
0
0
0
0
0
0
0
...
IN R18 PINA
R18 = 0
R18 = 1
R18 = 2
Delayed Nondeterminism
R18 = 3
HVC 2007
14
Delayed Nondeterminism
DDRA:
1
1
1
1
1
1
0
0
PORTA:
1
1
0
0
1
1
1
0
...
IN R18 PINA
R18 = 110011**
R18 = 110011**
SBRC R18 0
R18 = 110011*0
R18 = 110011*1
Delayed Nondeterminism
HVC 2007
15
The Formal Model: State Space
Bits: B := {0, 1}
Bytes: C := B8
Memory addresses: A := Cm (here: m = 2)
Nondeterministic bit value: ∗
B∗ := B ∪ {∗}, C∗ := B8∗
Deterministic addresses D ⊆ A
(certain registers, variables in formula, ...)
Memory states: V := {v | v : A → C∗ } where v(a) ∈ C for every a ∈ D
Control locations: Q (here: program counter)
(System) states: S := Q × V
Delayed Nondeterminism
HVC 2007
16
Flow of Control
In every cycle:
1
run environment handler g1 ; . . . ; gk
(introduces nondeterministic values where necessary),
2
if necessary, apply interrupt dispatcher e1 : q1 > . . . > el : ql
(reaction to extraordinary events such as interrupts); otherwise
3
apply instruction handler q : h1 : q01 > . . . > hm : q0m
for current location q ∈ Q
(normal execution of machine instructions)
Here each gi , hi is a guarded assignment of the form
e0 → x1 := e1 , . . . , xn := en
(ej value expressions, xj address expressions)
Delayed Nondeterminism
HVC 2007
17
Flow of Control
In every cycle:
1
run environment handler g1 ; . . . ; gk
(introduces nondeterministic values where necessary),
2
if necessary, apply interrupt dispatcher e1 : q1 > . . . > el : ql
(reaction to extraordinary events such as interrupts); otherwise
3
apply instruction handler q : h1 : q01 > . . . > hm : q0m
for current location q ∈ Q
(normal execution of machine instructions)
Here each gi , hi is a guarded assignment of the form
e0 → x1 := e1 , . . . , xn := en
(ej value expressions, xj address expressions)
Delayed Nondeterminism
HVC 2007
17
Flow of Control
In every cycle:
1
run environment handler g1 ; . . . ; gk
(introduces nondeterministic values where necessary),
2
if necessary, apply interrupt dispatcher e1 : q1 > . . . > el : ql
(reaction to extraordinary events such as interrupts); otherwise
3
apply instruction handler q : h1 : q01 > . . . > hm : q0m
for current location q ∈ Q
(normal execution of machine instructions)
Here each gi , hi is a guarded assignment of the form
e0 → x1 := e1 , . . . , xn := en
(ej value expressions, xj address expressions)
Delayed Nondeterminism
HVC 2007
17
Flow of Control
In every cycle:
1
run environment handler g1 ; . . . ; gk
(introduces nondeterministic values where necessary),
2
if necessary, apply interrupt dispatcher e1 : q1 > . . . > el : ql
(reaction to extraordinary events such as interrupts); otherwise
3
apply instruction handler q : h1 : q01 > . . . > hm : q0m
for current location q ∈ Q
(normal execution of machine instructions)
Here each gi , hi is a guarded assignment of the form
e0 → x1 := e1 , . . . , xn := en
(ej value expressions, xj address expressions)
Delayed Nondeterminism
HVC 2007
17
Example: Environment Handler
TCCR0[CS02] = 1 ∨ TCCR0[CS01] = 1 ∨ TCCR0[CS00] = 1
→ TIFR[TOV0] := nd(TIFR[TOV0]);
DDRB[DDB2] = 0 → GIFR[INTF2] := nd(GIFR[INTF2]); . . .
Timer overflow interrupt possible if timer activated
External interrupt possible if input enabled
Here: nd(∗) := ∗, nd(0) := ∗, and nd(1) := 1
Delayed Nondeterminism
HVC 2007
18
Example: Environment Handler
TCCR0[CS02] = 1 ∨ TCCR0[CS01] = 1 ∨ TCCR0[CS00] = 1
→ TIFR[TOV0] := nd(TIFR[TOV0]);
DDRB[DDB2] = 0 → GIFR[INTF2] := nd(GIFR[INTF2]); . . .
Timer overflow interrupt possible if timer activated
External interrupt possible if input enabled
Here: nd(∗) := ∗, nd(0) := ∗, and nd(1) := 1
Delayed Nondeterminism
HVC 2007
18
Example: Interrupt Dispatcher
SREG[I] = 1 ∧ TIMSK[TOIE0] = 1 ∧ TIFR[TOV0] = 1 : 18 >
SREG[I] = 1 ∧ GICR[INT2] = 1 ∧ GIFR[INTF2] = 1 : 36 > . . .
Timer interrupt raised if
interrupts are globally enabled and
timer interrupt not masked and
timer overflow has occurred
Effect: jump to interrupt handler at address 18
Delayed Nondeterminism
HVC 2007
19
Example: Interrupt Dispatcher
SREG[I] = 1 ∧ TIMSK[TOIE0] = 1 ∧ TIFR[TOV0] = 1 : 18 >
SREG[I] = 1 ∧ GICR[INT2] = 1 ∧ GIFR[INTF2] = 1 : 36 > . . .
Timer interrupt raised if
interrupts are globally enabled and
timer interrupt not masked and
timer overflow has occurred
Effect: jump to interrupt handler at address 18
Delayed Nondeterminism
HVC 2007
19
Example: Interrupt Dispatcher
SREG[I] = 1 ∧ TIMSK[TOIE0] = 1 ∧ TIFR[TOV0] = 1 : 18 >
SREG[I] = 1 ∧ GICR[INT2] = 1 ∧ GIFR[INTF2] = 1 : 36 > . . .
Timer interrupt raised if
interrupts are globally enabled and
timer interrupt not masked and
timer overflow has occurred
Effect: jump to interrupt handler at address 18
Delayed Nondeterminism
HVC 2007
19
Example: Interrupt Dispatcher
SREG[I] = 1 ∧ TIMSK[TOIE0] = 1 ∧ TIFR[TOV0] = 1 : 18 >
SREG[I] = 1 ∧ GICR[INT2] = 1 ∧ GIFR[INTF2] = 1 : 36 > . . .
Timer interrupt raised if
interrupts are globally enabled and
timer interrupt not masked and
timer overflow has occurred
Effect: jump to interrupt handler at address 18
Delayed Nondeterminism
HVC 2007
19
Example: Adding Instruction
ADD Ri,Rj at address q:
q : Ri := Ri + Rj, SREG[Z] := (Ri + Rj = 0), SREG[C] := . . . , . . . : q + 2
Adds contents of registers Ri and Rj and stores result in Ri
Sets flags in status register SREG:
zero flag Z (= 0)
carry flag C (= 1)
...
.+.:C×C→C
.=0:C→B
Delayed Nondeterminism
HVC 2007
20
Example: Adding Instruction
ADD Ri,Rj at address q:
q : Ri := Ri + Rj, SREG[Z] := (Ri + Rj = 0), SREG[C] := . . . , . . . : q + 2
Adds contents of registers Ri and Rj and stores result in Ri
Sets flags in status register SREG:
zero flag Z (= 0)
carry flag C (= 1)
...
.+.:C×C→C
.=0:C→B
Delayed Nondeterminism
HVC 2007
20
Example: Input Instruction
IN Ri,A at address q:
q : Ri := (DDRA ∧ PORTA) ∨ (¬DDRA ∧ PINA) : q + 2
Copies contents of registers PORTA/PINA according to mask DDRA
. ∧ . : C × C∗ → C∗
. ∨ . : C∗ × C∗ → C∗
¬. : C → C
Delayed Nondeterminism
HVC 2007
21
Example: “Skip If Bit Cleared” Instruction
SBRC Ri,b at address q:
q : Ri[b] = 0 →: q + 3 >
Ri[b] = 1 →: q + 2
Branches control according to bth bit in register Ri
Delayed Nondeterminism
HVC 2007
22
Immediate Instantiation I
Immediate Instantiation
Each assignment of nondeterministic bit values is resolved by assigning all
possible combinations of concrete values.
Thus: only deterministic values are allowed to be stored
Still v(a) ∈ C∗ \ C possible for specific addresses a ∈ A \ D
(e.g., a = PINA)
Guarded assignment g = q : e0 → x1 := e1 , . . . , xn := en : q0 enabled in
state (q, v) ∈ S if Je0 Kv = 1
g
Gives rise to concrete transition (q, v) −→ (q0 , v0 ) for every v0 ∈ V
obtained by
1
2
3
evaluating every right-hand side expression ei
taking every possible instantiation of nondeterministic bit values
updating v accordingly
Formally:
v0 := v[Jxi Kv 7→ ci ; 1 ≤ i ≤ n] with C ∪ B 3 ci v Jei Kv for all 1 ≤ i ≤ n
v ⊆ B∗ × B∗ given by 0 v ∗ and 1 v ∗ (pointwise lifted to C∗ and V)
=⇒ Yields concrete transition system T c = (S,
Delayed Nondeterminism
S
g
g∈G
−→, s0 )
HVC 2007
23
Immediate Instantiation I
Immediate Instantiation
Each assignment of nondeterministic bit values is resolved by assigning all
possible combinations of concrete values.
Thus: only deterministic values are allowed to be stored
Still v(a) ∈ C∗ \ C possible for specific addresses a ∈ A \ D
(e.g., a = PINA)
Guarded assignment g = q : e0 → x1 := e1 , . . . , xn := en : q0 enabled in
state (q, v) ∈ S if Je0 Kv = 1
g
Gives rise to concrete transition (q, v) −→ (q0 , v0 ) for every v0 ∈ V
obtained by
1
2
3
evaluating every right-hand side expression ei
taking every possible instantiation of nondeterministic bit values
updating v accordingly
Formally:
v0 := v[Jxi Kv 7→ ci ; 1 ≤ i ≤ n] with C ∪ B 3 ci v Jei Kv for all 1 ≤ i ≤ n
v ⊆ B∗ × B∗ given by 0 v ∗ and 1 v ∗ (pointwise lifted to C∗ and V)
=⇒ Yields concrete transition system T c = (S,
Delayed Nondeterminism
S
g
g∈G
−→, s0 )
HVC 2007
23
Immediate Instantiation I
Immediate Instantiation
Each assignment of nondeterministic bit values is resolved by assigning all
possible combinations of concrete values.
Thus: only deterministic values are allowed to be stored
Still v(a) ∈ C∗ \ C possible for specific addresses a ∈ A \ D
(e.g., a = PINA)
Guarded assignment g = q : e0 → x1 := e1 , . . . , xn := en : q0 enabled in
state (q, v) ∈ S if Je0 Kv = 1
g
Gives rise to concrete transition (q, v) −→ (q0 , v0 ) for every v0 ∈ V
obtained by
1
2
3
evaluating every right-hand side expression ei
taking every possible instantiation of nondeterministic bit values
updating v accordingly
Formally:
v0 := v[Jxi Kv 7→ ci ; 1 ≤ i ≤ n] with C ∪ B 3 ci v Jei Kv for all 1 ≤ i ≤ n
v ⊆ B∗ × B∗ given by 0 v ∗ and 1 v ∗ (pointwise lifted to C∗ and V)
=⇒ Yields concrete transition system T c = (S,
Delayed Nondeterminism
S
g
g∈G
−→, s0 )
HVC 2007
23
Immediate Instantiation I
Immediate Instantiation
Each assignment of nondeterministic bit values is resolved by assigning all
possible combinations of concrete values.
Thus: only deterministic values are allowed to be stored
Still v(a) ∈ C∗ \ C possible for specific addresses a ∈ A \ D
(e.g., a = PINA)
Guarded assignment g = q : e0 → x1 := e1 , . . . , xn := en : q0 enabled in
state (q, v) ∈ S if Je0 Kv = 1
g
Gives rise to concrete transition (q, v) −→ (q0 , v0 ) for every v0 ∈ V
obtained by
1
2
3
evaluating every right-hand side expression ei
taking every possible instantiation of nondeterministic bit values
updating v accordingly
Formally:
v0 := v[Jxi Kv 7→ ci ; 1 ≤ i ≤ n] with C ∪ B 3 ci v Jei Kv for all 1 ≤ i ≤ n
v ⊆ B∗ × B∗ given by 0 v ∗ and 1 v ∗ (pointwise lifted to C∗ and V)
=⇒ Yields concrete transition system T c = (S,
Delayed Nondeterminism
S
g
g∈G
−→, s0 )
HVC 2007
23
Immediate Instantiation I
Immediate Instantiation
Each assignment of nondeterministic bit values is resolved by assigning all
possible combinations of concrete values.
Thus: only deterministic values are allowed to be stored
Still v(a) ∈ C∗ \ C possible for specific addresses a ∈ A \ D
(e.g., a = PINA)
Guarded assignment g = q : e0 → x1 := e1 , . . . , xn := en : q0 enabled in
state (q, v) ∈ S if Je0 Kv = 1
g
Gives rise to concrete transition (q, v) −→ (q0 , v0 ) for every v0 ∈ V
obtained by
1
2
3
evaluating every right-hand side expression ei
taking every possible instantiation of nondeterministic bit values
updating v accordingly
Formally:
v0 := v[Jxi Kv 7→ ci ; 1 ≤ i ≤ n] with C ∪ B 3 ci v Jei Kv for all 1 ≤ i ≤ n
v ⊆ B∗ × B∗ given by 0 v ∗ and 1 v ∗ (pointwise lifted to C∗ and V)
=⇒ Yields concrete transition system T c = (S,
Delayed Nondeterminism
S
g
g∈G
−→, s0 )
HVC 2007
23
Immediate Instantiation I
Immediate Instantiation
Each assignment of nondeterministic bit values is resolved by assigning all
possible combinations of concrete values.
Thus: only deterministic values are allowed to be stored
Still v(a) ∈ C∗ \ C possible for specific addresses a ∈ A \ D
(e.g., a = PINA)
Guarded assignment g = q : e0 → x1 := e1 , . . . , xn := en : q0 enabled in
state (q, v) ∈ S if Je0 Kv = 1
g
Gives rise to concrete transition (q, v) −→ (q0 , v0 ) for every v0 ∈ V
obtained by
1
2
3
evaluating every right-hand side expression ei
taking every possible instantiation of nondeterministic bit values
updating v accordingly
Formally:
v0 := v[Jxi Kv 7→ ci ; 1 ≤ i ≤ n] with C ∪ B 3 ci v Jei Kv for all 1 ≤ i ≤ n
v ⊆ B∗ × B∗ given by 0 v ∗ and 1 v ∗ (pointwise lifted to C∗ and V)
=⇒ Yields concrete transition system T c = (S,
Delayed Nondeterminism
S
g
g∈G
−→, s0 )
HVC 2007
23
Immediate Instantiation II
Example
v(DDRA) = 11111100, v(PORTA) = 00000000,
v(PINA) = ∗ ∗ ∗ ∗ ∗ ∗ ∗ ∗
Execution of IN R1,A at address q:
q : R1 := (DDRA ∧ PORTA) ∨ (¬DDRA ∧ PINA) : q + 2
Transitions from (q, v) to
1
2
3
4
(q + 2, v[R1 7→ 00000000])
(q + 2, v[R1 7→ 00000001])
(q + 2, v[R1 7→ 00000010])
(q + 2, v[R1 7→ 00000011])
Delayed Nondeterminism
HVC 2007
24
Immediate Instantiation II
Example
v(DDRA) = 11111100, v(PORTA) = 00000000,
v(PINA) = ∗ ∗ ∗ ∗ ∗ ∗ ∗ ∗
Execution of IN R1,A at address q:
q : R1 := (DDRA ∧ PORTA) ∨ (¬DDRA ∧ PINA) : q + 2
Transitions from (q, v) to
1
2
3
4
(q + 2, v[R1 7→ 00000000])
(q + 2, v[R1 7→ 00000001])
(q + 2, v[R1 7→ 00000010])
(q + 2, v[R1 7→ 00000011])
Delayed Nondeterminism
HVC 2007
24
Immediate Instantiation II
Example
v(DDRA) = 11111100, v(PORTA) = 00000000,
v(PINA) = ∗ ∗ ∗ ∗ ∗ ∗ ∗ ∗
Execution of IN R1,A at address q:
q : R1 := (DDRA ∧ PORTA) ∨ (¬DDRA ∧ PINA) : q + 2
Transitions from (q, v) to
1
2
3
4
(q + 2, v[R1 7→ 00000000])
(q + 2, v[R1 7→ 00000001])
(q + 2, v[R1 7→ 00000010])
(q + 2, v[R1 7→ 00000011])
Delayed Nondeterminism
HVC 2007
24
Delayed Nondeterminism I
Delayed Nondeterminism
Replace nondeterministic by concrete values only if and when this is required
by a subsequent computation step.
Delayed Nondeterminism
HVC 2007
25
Delayed Nondeterminism II
Informally: instantiation of
v(a)[b] = ∗ in (q, v) ∈ S
required when ex.
g = q : e0 → x1 :=
e1 , . . . , xn := en : q0 s.t.
Formally: g induces abstract transition
g
(q, v) =⇒ (q0 , v0 ) if ex. v1 , v2 , v3 , v4 ∈ V s.t.
1
2
(a, b) referred by e0 , or
g enabled and some ei
refers to (a, b) in a
deterministic argument,
or
some xi dereferences a,
or
some ei yields ∗ and xi
deterministic
3
4
5
6
v1 v v with v1 (a, b) 6= ∗ if (a, b) referred by
e0 , and
Je0 Kv1 = 1, and
v2 v v1 with v2 (a, b) 6= ∗ if some
ei = op(y1 , . . . , yn ), op : T1 × . . . × Tn → T0 ,
and (a, b) referred by some yj where
Tj ∈ {C, B}, and
v3 v v2 with v3 (a, b) 6= ∗ if some
xi = a↓ + d, and
v4 := v3 [Jxi Kv3 7→ Jei Kv3 ; 1 ≤ i ≤ n], and
v0 ≤ v4 with v0 (a, b) 6= ∗ if
Jxi Kv4 ∈ {a, (a, b)} for some i, a ∈ D
=⇒ Yields abstract transition system T a = (S,
Delayed Nondeterminism
S
g
g∈G
=⇒, s0 )
HVC 2007
26
Delayed Nondeterminism II
Informally: instantiation of
v(a)[b] = ∗ in (q, v) ∈ S
required when ex.
g = q : e0 → x1 :=
e1 , . . . , xn := en : q0 s.t.
(a, b) referred by e0 , or
g enabled and some ei
refers to (a, b) in a
deterministic argument,
or
some xi dereferences a,
or
some ei yields ∗ and xi
deterministic
Formally: g induces abstract transition
g
(q, v) =⇒ (q0 , v0 ) if ex. v1 , v2 , v3 , v4 ∈ V s.t.
1
v1 v v with v1 (a, b) 6= ∗ if (a, b) referred by
e0 , and
2
Je0 Kv1 = 1, and
3
4
5
6
v2 v v1 with v2 (a, b) 6= ∗ if some
ei = op(y1 , . . . , yn ), op : T1 × . . . × Tn → T0 ,
and (a, b) referred by some yj where
Tj ∈ {C, B}, and
v3 v v2 with v3 (a, b) 6= ∗ if some
xi = a↓ + d, and
v4 := v3 [Jxi Kv3 7→ Jei Kv3 ; 1 ≤ i ≤ n], and
v0 ≤ v4 with v0 (a, b) 6= ∗ if
Jxi Kv4 ∈ {a, (a, b)} for some i, a ∈ D
=⇒ Yields abstract transition system T a = (S,
Delayed Nondeterminism
S
g
g∈G
=⇒, s0 )
HVC 2007
26
Delayed Nondeterminism II
Informally: instantiation of
v(a)[b] = ∗ in (q, v) ∈ S
required when ex.
g = q : e0 → x1 :=
e1 , . . . , xn := en : q0 s.t.
(a, b) referred by e0 , or
g enabled and some ei
refers to (a, b) in a
deterministic argument,
or
some xi dereferences a,
or
some ei yields ∗ and xi
deterministic
Formally: g induces abstract transition
g
(q, v) =⇒ (q0 , v0 ) if ex. v1 , v2 , v3 , v4 ∈ V s.t.
1
v1 v v with v1 (a, b) 6= ∗ if (a, b) referred by
e0 , and
2
Je0 Kv1 = 1, and
3
v2 v v1 with v2 (a, b) 6= ∗ if some
ei = op(y1 , . . . , yn ), op : T1 × . . . × Tn → T0 ,
and (a, b) referred by some yj where
Tj ∈ {C, B}, and
4
v3 v v2 with v3 (a, b) 6= ∗ if some
xi = a↓ + d, and
5
v4 := v3 [Jxi Kv3 7→ Jei Kv3 ; 1 ≤ i ≤ n], and
v0 ≤ v4 with v0 (a, b) 6= ∗ if
Jxi Kv4 ∈ {a, (a, b)} for some i, a ∈ D
6
=⇒ Yields abstract transition system T a = (S,
Delayed Nondeterminism
S
g
g∈G
=⇒, s0 )
HVC 2007
26
Delayed Nondeterminism II
Informally: instantiation of
v(a)[b] = ∗ in (q, v) ∈ S
required when ex.
g = q : e0 → x1 :=
e1 , . . . , xn := en : q0 s.t.
(a, b) referred by e0 , or
g enabled and some ei
refers to (a, b) in a
deterministic argument,
or
some xi dereferences a,
or
some ei yields ∗ and xi
deterministic
Formally: g induces abstract transition
g
(q, v) =⇒ (q0 , v0 ) if ex. v1 , v2 , v3 , v4 ∈ V s.t.
1
v1 v v with v1 (a, b) 6= ∗ if (a, b) referred by
e0 , and
2
Je0 Kv1 = 1, and
3
v2 v v1 with v2 (a, b) 6= ∗ if some
ei = op(y1 , . . . , yn ), op : T1 × . . . × Tn → T0 ,
and (a, b) referred by some yj where
Tj ∈ {C, B}, and
4
v3 v v2 with v3 (a, b) 6= ∗ if some
xi = a↓ + d, and
5
v4 := v3 [Jxi Kv3 7→ Jei Kv3 ; 1 ≤ i ≤ n], and
v0 ≤ v4 with v0 (a, b) 6= ∗ if
Jxi Kv4 ∈ {a, (a, b)} for some i, a ∈ D
6
=⇒ Yields abstract transition system T a = (S,
Delayed Nondeterminism
S
g
g∈G
=⇒, s0 )
HVC 2007
26
Delayed Nondeterminism II
Informally: instantiation of
v(a)[b] = ∗ in (q, v) ∈ S
required when ex.
g = q : e0 → x1 :=
e1 , . . . , xn := en : q0 s.t.
(a, b) referred by e0 , or
g enabled and some ei
refers to (a, b) in a
deterministic argument,
or
some xi dereferences a,
or
some ei yields ∗ and xi
deterministic
Formally: g induces abstract transition
g
(q, v) =⇒ (q0 , v0 ) if ex. v1 , v2 , v3 , v4 ∈ V s.t.
1
v1 v v with v1 (a, b) 6= ∗ if (a, b) referred by
e0 , and
2
Je0 Kv1 = 1, and
3
v2 v v1 with v2 (a, b) 6= ∗ if some
ei = op(y1 , . . . , yn ), op : T1 × . . . × Tn → T0 ,
and (a, b) referred by some yj where
Tj ∈ {C, B}, and
4
v3 v v2 with v3 (a, b) 6= ∗ if some
xi = a↓ + d, and
5
v4 := v3 [Jxi Kv3 7→ Jei Kv3 ; 1 ≤ i ≤ n], and
v0 ≤ v4 with v0 (a, b) 6= ∗ if
Jxi Kv4 ∈ {a, (a, b)} for some i, a ∈ D
6
=⇒ Yields abstract transition system T a = (S,
Delayed Nondeterminism
S
g
g∈G
=⇒, s0 )
HVC 2007
26
Delayed Nondeterminism II
Informally: instantiation of
v(a)[b] = ∗ in (q, v) ∈ S
required when ex.
g = q : e0 → x1 :=
e1 , . . . , xn := en : q0 s.t.
(a, b) referred by e0 , or
g enabled and some ei
refers to (a, b) in a
deterministic argument,
or
some xi dereferences a,
or
some ei yields ∗ and xi
deterministic
Formally: g induces abstract transition
g
(q, v) =⇒ (q0 , v0 ) if ex. v1 , v2 , v3 , v4 ∈ V s.t.
1
v1 v v with v1 (a, b) 6= ∗ if (a, b) referred by
e0 , and
2
Je0 Kv1 = 1, and
3
v2 v v1 with v2 (a, b) 6= ∗ if some
ei = op(y1 , . . . , yn ), op : T1 × . . . × Tn → T0 ,
and (a, b) referred by some yj where
Tj ∈ {C, B}, and
4
v3 v v2 with v3 (a, b) 6= ∗ if some
xi = a↓ + d, and
5
v4 := v3 [Jxi Kv3 7→ Jei Kv3 ; 1 ≤ i ≤ n], and
v0 ≤ v4 with v0 (a, b) 6= ∗ if
Jxi Kv4 ∈ {a, (a, b)} for some i, a ∈ D
6
=⇒ Yields abstract transition system T a = (S,
Delayed Nondeterminism
S
g
g∈G
=⇒, s0 )
HVC 2007
26
Delayed Nondeterminism III
Example
v(DDRA) = 11111100, v(PORTA) = 00000000,
v(PINA) = ∗ ∗ ∗ ∗ ∗ ∗ ∗ ∗
Execution of IN R1,A at address q:
q : R1 := (DDRA ∧ PORTA) ∨ (¬DDRA ∧ PINA) : q + 2
yields transition (q, v) =⇒ (q + 2, v[R1 7→ 000000 ∗ ∗])
| {z } |
{z
}
q0
Execution of SBRC R1,0 at address
v0
q0 :
q0 : R1[0] = 0 →: q0 + 3
q0 : R1[0] = 1 →: q0 + 2
yields (q0 , v0 ) =⇒ (q0 + 3, v[R1 7→ 000000 ∗ 0])
and (q0 , v0 ) =⇒ (q0 + 2, v[R1 7→ 000000 ∗ 1])
Delayed Nondeterminism
HVC 2007
27
Delayed Nondeterminism III
Example
v(DDRA) = 11111100, v(PORTA) = 00000000,
v(PINA) = ∗ ∗ ∗ ∗ ∗ ∗ ∗ ∗
Execution of IN R1,A at address q:
q : R1 := (DDRA ∧ PORTA) ∨ (¬DDRA ∧ PINA) : q + 2
yields transition (q, v) =⇒ (q + 2, v[R1 7→ 000000 ∗ ∗])
| {z } |
{z
}
q0
Execution of SBRC R1,0 at address
v0
q0 :
q0 : R1[0] = 0 →: q0 + 3
q0 : R1[0] = 1 →: q0 + 2
yields (q0 , v0 ) =⇒ (q0 + 3, v[R1 7→ 000000 ∗ 0])
and (q0 , v0 ) =⇒ (q0 + 2, v[R1 7→ 000000 ∗ 1])
Delayed Nondeterminism
HVC 2007
27
Delayed Nondeterminism III
Example
v(DDRA) = 11111100, v(PORTA) = 00000000,
v(PINA) = ∗ ∗ ∗ ∗ ∗ ∗ ∗ ∗
Execution of IN R1,A at address q:
q : R1 := (DDRA ∧ PORTA) ∨ (¬DDRA ∧ PINA) : q + 2
yields transition (q, v) =⇒ (q + 2, v[R1 7→ 000000 ∗ ∗])
| {z } |
{z
}
q0
Execution of SBRC R1,0 at address
v0
q0 :
q0 : R1[0] = 0 →: q0 + 3
q0 : R1[0] = 1 →: q0 + 2
yields (q0 , v0 ) =⇒ (q0 + 3, v[R1 7→ 000000 ∗ 0])
and (q0 , v0 ) =⇒ (q0 + 2, v[R1 7→ 000000 ∗ 1])
Delayed Nondeterminism
HVC 2007
27
Soundness of Abstraction I
Property specification given by temporal formula ϕ over set P of bit
value expressions
Defines labeling λ : S → 2P : (q, v) 7→ {p ∈ P | JpKv = 1}
S
g
concrete LTS: Lc = (S, g∈G −→, s0 , λ)
S
g
abstract LTS: La = (S, g∈G =⇒, s0 , λ)
note: JpKv always defined since Var(ϕ) ⊆ D
Connection between Lc and La given by simulation:
a binary relation ρ ⊆ S × S such that s0 ρs0 and, whenever s1 ρs2 ,
λ(s1 ) = λ(s2 ) and
g
for every transition s1 −→ s01
0
there exists s2 ∈ S
g
such that s2 =⇒ s02 and s01 ρs02
Delayed Nondeterminism
HVC 2007
28
Soundness of Abstraction I
Property specification given by temporal formula ϕ over set P of bit
value expressions
Defines labeling λ : S → 2P : (q, v) 7→ {p ∈ P | JpKv = 1}
S
g
concrete LTS: Lc = (S, g∈G −→, s0 , λ)
S
g
abstract LTS: La = (S, g∈G =⇒, s0 , λ)
note: JpKv always defined since Var(ϕ) ⊆ D
Connection between Lc and La given by simulation:
a binary relation ρ ⊆ S × S such that s0 ρs0 and, whenever s1 ρs2 ,
λ(s1 ) = λ(s2 ) and
g
for every transition s1 −→ s01
0
there exists s2 ∈ S
g
such that s2 =⇒ s02 and s01 ρs02
Delayed Nondeterminism
HVC 2007
28
Soundness of Abstraction II
Theorem
La simulates Lc .
Proof.
Simulation relation given by partial order on bit values:
(q1 , v1 )ρ(q2 , v2 ) iff q1 = q2 and v1 v v2
Corollary
Delayed nondeterminism is sound w.r.t. “path-universal” temporal logics
such as LTL or ACTL:
La |= ϕ implies Lc |= ϕ
(i.e., no false positives)
Delayed Nondeterminism
HVC 2007
29
Soundness of Abstraction II
Theorem
La simulates Lc .
Proof.
Simulation relation given by partial order on bit values:
(q1 , v1 )ρ(q2 , v2 ) iff q1 = q2 and v1 v v2
Corollary
Delayed nondeterminism is sound w.r.t. “path-universal” temporal logics
such as LTL or ACTL:
La |= ϕ implies Lc |= ϕ
(i.e., no false positives)
Delayed Nondeterminism
HVC 2007
29
Soundness of Abstraction II
Theorem
La simulates Lc .
Proof.
Simulation relation given by partial order on bit values:
(q1 , v1 )ρ(q2 , v2 ) iff q1 = q2 and v1 v v2
Corollary
Delayed nondeterminism is sound w.r.t. “path-universal” temporal logics
such as LTL or ACTL:
La |= ϕ implies Lc |= ϕ
(i.e., no false positives)
Delayed Nondeterminism
HVC 2007
29
Empirical Results
Program
light switch
plant
reentrance
problem
traffic light
window lift
Instantiation# states stored# states createdSize [MB]Time [s]Reduction
immediate
6,624
9,050
2
0.2
delayed
352
380
<1
0.01
95%
immediate
801,616
854,203
256
23.19
delayed
188,404
195,955
61
5.05
76%
immediate
107,649
110,961
33
2.8
delayed
107,649
110,961
33
2.8
0%
immediate
35,613
38,198
11
0.92
delayed
10,004
10,520
3
0.28
72%
immediate 10,100,400
11,196,174
2,049 416.98
delayed
323,450
444,191
102
10.78
97%
Delayed Nondeterminism
HVC 2007
30
Conclusion
Delayed Nondeterminism: abstraction technique for explicit-state model
checking of microcontroller code
(similar to “X-valued simulation” in hardware verification)
Significant reduction of state space in concrete examples
Over-approximation:
sound for path-universal logics (simulation)
generally incomplete (false negatives due to copying of nondeterminism)
Future work:
handle more microcontrollers (Infineon Tricore, Intel MC, ...)
establish bisimulation by introducing identities for nondeterministic values
implement compiler generator for state-space evaluators
Delayed Nondeterminism
HVC 2007
31
Conclusion
Delayed Nondeterminism: abstraction technique for explicit-state model
checking of microcontroller code
(similar to “X-valued simulation” in hardware verification)
Significant reduction of state space in concrete examples
Over-approximation:
sound for path-universal logics (simulation)
generally incomplete (false negatives due to copying of nondeterminism)
Future work:
handle more microcontrollers (Infineon Tricore, Intel MC, ...)
establish bisimulation by introducing identities for nondeterministic values
implement compiler generator for state-space evaluators
Delayed Nondeterminism
HVC 2007
31
Conclusion
Delayed Nondeterminism: abstraction technique for explicit-state model
checking of microcontroller code
(similar to “X-valued simulation” in hardware verification)
Significant reduction of state space in concrete examples
Over-approximation:
sound for path-universal logics (simulation)
generally incomplete (false negatives due to copying of nondeterminism)
Future work:
handle more microcontrollers (Infineon Tricore, Intel MC, ...)
establish bisimulation by introducing identities for nondeterministic values
implement compiler generator for state-space evaluators
Delayed Nondeterminism
HVC 2007
31
Conclusion
Delayed Nondeterminism: abstraction technique for explicit-state model
checking of microcontroller code
(similar to “X-valued simulation” in hardware verification)
Significant reduction of state space in concrete examples
Over-approximation:
sound for path-universal logics (simulation)
generally incomplete (false negatives due to copying of nondeterminism)
Future work:
handle more microcontrollers (Infineon Tricore, Intel MC, ...)
establish bisimulation by introducing identities for nondeterministic values
implement compiler generator for state-space evaluators
Delayed Nondeterminism
HVC 2007
31
Incompleteness of Abstraction
Observation: over-approximation due to copying of nondeterminism
Example
q1 :
a[0] := ∗ : q2
q2 :
a[1] := a[0]: q3
q3 : a[0] ∧ ¬a[1] →
: q4
q1
q2
q3
Immediate
•
. &
a[0] = 0
a[0] = 1
↓
↓
a[0] = a[1] = 0 a[0] = a[1] = 1
6↓
6↓
q4
Delayed
•
↓
a[0] = ∗
↓
a[0] = a[1] = ∗
↓
a[0] = 1, a[1] = 0 "
=⇒ false negatives possible
Delayed Nondeterminism
HVC 2007
32
Incompleteness of Abstraction
Observation: over-approximation due to copying of nondeterminism
Example
q1 :
a[0] := ∗ : q2
q2 :
a[1] := a[0]: q3
q3 : a[0] ∧ ¬a[1] →
: q4
q1
q2
q3
Immediate
•
. &
a[0] = 0
a[0] = 1
↓
↓
a[0] = a[1] = 0 a[0] = a[1] = 1
6↓
6↓
q4
Delayed
•
↓
a[0] = ∗
↓
a[0] = a[1] = ∗
↓
a[0] = 1, a[1] = 0 "
=⇒ false negatives possible
Delayed Nondeterminism
HVC 2007
32
Incompleteness of Abstraction
Observation: over-approximation due to copying of nondeterminism
Example
q1 :
a[0] := ∗ : q2
q2 :
a[1] := a[0]: q3
q3 : a[0] ∧ ¬a[1] →
: q4
q1
q2
q3
Immediate
•
. &
a[0] = 0
a[0] = 1
↓
↓
a[0] = a[1] = 0 a[0] = a[1] = 1
6↓
6↓
q4
Delayed
•
↓
a[0] = ∗
↓
a[0] = a[1] = ∗
↓
a[0] = 1, a[1] = 0 "
=⇒ false negatives possible
Delayed Nondeterminism
HVC 2007
32
Incompleteness of Abstraction
Observation: over-approximation due to copying of nondeterminism
Example
q1 :
a[0] := ∗ : q2
q2 :
a[1] := a[0]: q3
q3 : a[0] ∧ ¬a[1] →
: q4
q1
q2
q3
Immediate
•
. &
a[0] = 0
a[0] = 1
↓
↓
a[0] = a[1] = 0 a[0] = a[1] = 1
6↓
6↓
q4
Delayed
•
↓
a[0] = ∗
↓
a[0] = a[1] = ∗
↓
a[0] = 1, a[1] = 0 "
=⇒ false negatives possible
Delayed Nondeterminism
HVC 2007
32
Incompleteness of Abstraction
Observation: over-approximation due to copying of nondeterminism
Example
q1 :
a[0] := ∗ : q2
q2 :
a[1] := a[0]: q3
q3 : a[0] ∧ ¬a[1] →
: q4
q1
q2
q3
Immediate
•
. &
a[0] = 0
a[0] = 1
↓
↓
a[0] = a[1] = 0 a[0] = a[1] = 1
6↓
6↓
q4
Delayed
•
↓
a[0] = ∗
↓
a[0] = a[1] = ∗
↓
a[0] = 1, a[1] = 0 "
=⇒ false negatives possible
Delayed Nondeterminism
HVC 2007
32
Incompleteness of Abstraction
Observation: over-approximation due to copying of nondeterminism
Example
q1 :
a[0] := ∗ : q2
q2 :
a[1] := a[0]: q3
q3 : a[0] ∧ ¬a[1] →
: q4
q1
q2
q3
Immediate
•
. &
a[0] = 0
a[0] = 1
↓
↓
a[0] = a[1] = 0 a[0] = a[1] = 1
6↓
6↓
q4
Delayed
•
↓
a[0] = ∗
↓
a[0] = a[1] = ∗
↓
a[0] = 1, a[1] = 0 "
=⇒ false negatives possible
Delayed Nondeterminism
HVC 2007
32