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