Diploma Thesis: Michael Rohrbach

MCESS

Model Checking For Embedded Systems Software

Abstract

Nowadays verification of software gets more and more important, especially in the field of embedded systems, like automotive software, where errors can lead to expensive callbacks.
The goal of this diploma thesis is the development and implementation of a C Code Model Checker for embedded systems software. Although there are already some C Code Model Checkers available, these tools are not applicable to embedded systems because of the special nature of microcontroller programs. A Model Checker for embedded systems has to support special features like direct memory access, interrupt handling, inlined assembler instructions, usage of timers, communication interfaces and so on.
In this approach the analyzed program is first compiled to its assembly code representation. That way the C source code and inlined assembler instruction can be treated simultaneously, in addition to that complicated C control structures are translated to simple jump instructions. Another advantage is that the model checker verifies the code which is actually executed on the microcontroller, including erros introduced by the compiler.
The state space generation of the microcontroller program is done by means of the NIPS VM, a virtual machine for state space generation. Thus the next step consists of a further translation from the assembly code to the so called NIPS VM bytecode. The bytecode is the basis for all following steps like static analyses, state space generation, and Model Checking.
Initially the model checker will support programs for the Atmel ATmega16 microcontroller, but the Model Checker is designed to be easily adapted to other microcontrollers. To obtain this, the model checker gets a complete specification of the used microcontroller in addition to the analyzed program. The specification basically consists of the memory layout, instruction semantics and abstractions for hardware features of the microcontroller. For this purpose a language was developed which is based on the register transfer language (RTL) and uses information which can easily be found in every microcontroller documentation to make the specification of a new microcontroller as easy as possible.

Example

Consider the following example program:

volatile int i=0;
char in_interrupt_handler = 0;

int main (void){
  // PORTA as output
  DDRA = 0xFF;
  PORTA = 0xFF;

  // IR 2 with falling edge
  MCUCSR = MCUCSR | (1<<ISC2);
  // ext IR 2 activated
  GICR = GICR | (1<<INT2);

  // global IR enable
  sei();

  while (1){
    while(i < 300){
                                     sts 0x0062, r25
      i++;
                                     sts 0x0061, r24
    }
    i = 0;
  }
}

SIGNAL (SIG_INTERRUPT2){
  in_interrupt_handler = 1;
  if (i < 150)
    PORTA = 0x00;
  else if (i < 300)
    PORTA = 0x55;

  PORTA = 0xFF;
  in_interrupt_handler = 0;
}
with the formula

[] ((in_interrupt_handler == 1) -> (i >= 0 && i <= 300))

meaning that each time the microcontroller executes the code of the interrupt handler, the value of i is greater or equal to 0 and less or equal to 300. Looking at the C source code, the formula seems to be true. But if you look at the translation of i++ you see that it yields two assembler instructions to store the 2-byte integer variable bytewise. Since the interrupt can be triggered after each assembler instruction the formula is not fulfilled.
The Model Checker returns the following counterexample (extract):
.
.
.
-------------------- variables --------------------
|          name           |   O   |  S  |  value  |
---------------------------------------------------
| i                       |    97 |   2 |     255 |
| in_interrupt_handler    |    96 |   1 |       0 |
---------------------------------------------------
-------------------- registers --------------------
| 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 |
| 00 00 00 00 00 00 00 00 00 01 63 00 5F 04 28 01 |
| 00 F8 FE FF 00 00 00 00 00 00 20 00 00 00 00 00 |
| 00 00 00 00 00 00 00 00 00 00 FF FF 00 00 00 00 |
| 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 |
| 00 00 00 00 40 00 00 00 00 00 00 20 00 5F 04 A0 |
---------------------------------------------------
----------------------------------------------------- processes -----------------------------------------------------
|          name          |               c source               |                od source             | nipsvm pc  |
---------------------------------------------------------------------------------------------------------------------
| main program           |                                 i++; |                   0x194: sts 98, r25 | 0x000009A9 |
| interrupt handler 0    |                                      |     0x3: int. handler 18 executable? | 0x00001F79 |
---------------------------------------------------------------------------------------------------------------------

--- process 0 sts 98, r25 --->

-------------------- variables --------------------
|          name           |   O   |  S  |  value  |
---------------------------------------------------
| i                       |    97 |   2 |     511 |
| in_interrupt_handler    |    96 |   1 |       0 |
---------------------------------------------------
-------------------- registers --------------------
| 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 |
| 00 00 00 00 00 00 00 00 00 01 63 00 5F 04 28 01 |
| 00 F8 FE FF 00 00 00 00 00 00 20 00 00 00 00 00 |
| 00 00 00 00 00 00 00 00 00 00 FF FF 00 00 00 00 |
| 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 |
| 00 00 00 00 40 00 00 00 00 00 00 20 00 5F 04 A0 |
---------------------------------------------------
----------------------------------------------------- processes -----------------------------------------------------
|          name          |               c source               |                od source             | nipsvm pc  |
---------------------------------------------------------------------------------------------------------------------
| main program           |                                 i++; |                   0x198: sts 97, r24 | 0x000009F6 |
| interrupt handler 0    |                                      |     0x3: int. handler 18 executable? | 0x00001F79 |
---------------------------------------------------------------------------------------------------------------------

--- process 1 int. handler 18 executable? --->

-------------------- variables --------------------
|          name           |   O   |  S  |  value  |
---------------------------------------------------
| i                       |    97 |   2 |     511 |
| in_interrupt_handler    |    96 |   1 |       0 |
---------------------------------------------------
-------------------- registers --------------------
| 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 |
| 00 00 00 00 00 00 00 00 00 01 63 00 5F 04 28 01 |
| 00 F8 FE FF 00 00 00 00 00 00 20 00 00 00 00 00 |
| 00 00 00 00 00 00 00 00 00 00 FF FF 00 00 00 00 |
| 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 |
| 00 00 00 00 40 00 00 00 00 00 00 20 00 5D 04 20 |
---------------------------------------------------
----------------------------------------------------- processes -----------------------------------------------------
|          name          |               c source               |                od source             | nipsvm pc  |
---------------------------------------------------------------------------------------------------------------------
| main program           |                                 i++; |                   0x198: sts 97, r24 | 0x000009F6 |
| interrupt handler 0    |             SIGNAL (SIG_INTERRUPT2){ |                       0x214: push r1 | 0x00001150 |
---------------------------------------------------------------------------------------------------------------------

.
.
.

-------------------- variables --------------------
|          name           |   O   |  S  |  value  |
---------------------------------------------------
| i                       |    97 |   2 |     511 |
| in_interrupt_handler    |    96 |   1 |       0 |
---------------------------------------------------
-------------------- registers --------------------
| 20 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 |
| 00 00 00 00 00 00 00 00 00 01 63 00 5F 04 28 01 |
| 00 F8 FE FF 00 00 00 00 00 00 20 00 00 00 00 00 |
| 00 00 00 00 00 00 00 00 00 00 FF FF 00 00 00 00 |
| 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 |
| 00 00 00 00 40 00 00 00 00 00 00 20 00 57 04 22 |
---------------------------------------------------
----------------------------------------------------- processes -----------------------------------------------------
|          name          |               c source               |                od source             | nipsvm pc  |
---------------------------------------------------------------------------------------------------------------------
| main program           |                                 i++; |                   0x198: sts 97, r24 | 0x000009F6 |
| interrupt handler 0    |            in_interrupt_handler = 1; |                    0x230: ldi r24, 1 | 0x00001441 |
---------------------------------------------------------------------------------------------------------------------

--- process 1 ldi r24, 1 --->

-------------------- variables --------------------
|          name           |   O   |  S  |  value  |
---------------------------------------------------
| i                       |    97 |   2 |     511 |
| in_interrupt_handler    |    96 |   1 |       0 |
---------------------------------------------------
-------------------- registers --------------------
| 20 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 |
| 00 00 00 00 00 00 00 00 01 01 63 00 5F 04 28 01 |
| 00 F8 FE FF 00 00 00 00 00 00 20 00 00 00 00 00 |
| 00 00 00 00 00 00 00 00 00 00 FF FF 00 00 00 00 |
| 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 |
| 00 00 00 00 40 00 00 00 00 00 00 20 00 57 04 22 |
---------------------------------------------------
----------------------------------------------------- processes -----------------------------------------------------
|          name          |               c source               |                od source             | nipsvm pc  |
---------------------------------------------------------------------------------------------------------------------
| main program           |                                 i++; |                   0x198: sts 97, r24 | 0x000009F6 |
| interrupt handler 0    |            in_interrupt_handler = 1; |                   0x232: sts 96, r24 | 0x00001485 |
---------------------------------------------------------------------------------------------------------------------

--- process 1 sts 96, r24; process 2 (no command information) --->

-------------------- variables --------------------
|          name           |   O   |  S  |  value  |
---------------------------------------------------
| i                       |    97 |   2 |     511 |
| in_interrupt_handler    |    96 |   1 |       1 |
---------------------------------------------------
-------------------- registers --------------------
| 20 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 |
| 00 00 00 00 00 00 00 00 01 01 63 00 5F 04 28 01 |
| 00 F8 FE FF 00 00 00 00 00 00 20 00 00 00 00 00 |
| 00 00 00 00 00 00 00 00 00 00 FF FF 00 00 00 00 |
| 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 |
| 00 00 00 00 40 00 00 00 00 00 00 20 00 57 04 22 |
---------------------------------------------------
----------------------------------------------------- processes -----------------------------------------------------
|          name          |               c source               |                od source             | nipsvm pc  |
---------------------------------------------------------------------------------------------------------------------
| main program           |                                 i++; |                   0x198: sts 97, r24 | 0x000009F6 |
| interrupt handler 0    |                         if (i < 150) |                   0x236: lds r24, 97 | 0x000014CA |
---------------------------------------------------------------------------------------------------------------------
It shows that if i has the value 255=0x00FF and the next value 256=0x0100 has to be stored to the corresponding memory lcoation, the execution of the first sts instruction yields the value 511=0x01FF for i. If the interrupt is triggered in this state, the execution of the interrupt handler code finally leads to a state which falsifies the formula.