## Checksum property for AUTOSAR

Property based testing is based upon the idea that one writes a property about the software under tests and from that property the tool QuickCheck automatically generates test cases to test your software.

Properties can be difficult to formulate, since a lot of software has grown and the once clear ideas have been polluted and clear properties have been obfuscated. That is, if the software has not been developed using property based development. However, there is a simple property that comes in handy very often: one version of the software should for a certain input domain be the same as a different version. This comparison with other versions or even other implementations can often reveal errors introduced by optimizations or compatibility issues between competing implementations.

In this post we take a simple example of a table based implementation and a computation based computation of a checksum algorithm. The example was motivated by the implementation of the CRC library in the AUTOSAR standard. Two differently configured C programs should give equal results on the same input. This is a commonly occurring phenomena, but the solution presented is kept simple and does not take stateful systems into account; this extension is possible and subject for a later post.

## Modelling CRC routines

Computing checksums is based on mathematical theory where CRC-Algorithms are related to polynomials with coefficients in the finite field of two elements. The Hamming Distance, i.e., the number of bits that an be detected to have changed, is determined by the generator polynomial chosen. The AUTOSAR specification explains these algorithms in general terms and provides some optimizations for specific values.

It is important to realize that the AUTOSAR specification specifies a family of CRC functions that are parametrised in several ways. The specification furthermore provides allowed subsets in the parameter space. Different End-to-End implementations are required to use different CRC functions or the same function with different parameters. We describe a QuickCheck model for the CRC CalculateCRC8 function. This function has fixed the CRC result to 8 bits, a polynomial with value 0x1D, an inital value 0xFF, no input reflection nor result data reflection, and an XOR value of 0xFF.

The CRC-Algorithms have some mathematical properties that can be used as weak validators of implementations of the algorithms. These properties provide a simple mechanism to see if the implementation computes a correct value in a number of data points. The first ‘property’ is Check, stating that if the implementation is given the ASCII values ”123456789” then it should return the value 0x4B. The second property is Magic Check, which is a check for any data sequence. Given a number of bytes, compute the checksum, compute the checksum over data plus checksum and XOR that with 0xFF. The result for CRC_CalculateCRC8 should always be 0xC4.
Clearly, Check is just one test case, whereas Magic Check is a property that describes a large number of possible test cases that all should result in the same value 0xC4.

## Mathematical properties in Erlang and QuickCheck

Now assume that we have a C implementation of the function CRC_CalculateCRC8 with prototype as specified in the AUTOSAR standard:

```uint8 Crc_CalculateCRC8(const uint8* Crc_DataPtr, uint32 Crc_Length,
uint8 Crc_StartValue8, boolean Crc_IsFirstCall)
```

The first argument is a pointer to the data, the second argument the number of bytes in the data block, the third argument is a start value which is only used if the calculation uses multiple calls to this function, in which case the fourth argument should be set to false.

Performing the Check property in Erlang and QuickCheck is done as follows. First one links the C implementation to the test framework by calling the function eqc_c:start(’Crc’), given that the name of the C module is ”Crc.c”. The above mentioned CRC_CalculateCRC8 function is now accessible and call be called from the framework.

The test case is constructed in Erlang by first allocating some memory in the C threat the C program is running in, putting the data ”123456789” in that memory location and calling the function with arguments: 9 bytes long data, initial value 0xFF as defined by the standard and 1 (TRUE) for the last argument. The test cases looks in Erlang and QuickCheck as:

```check() ->
Ptr   = eqc_c:create_array("uint8","123456789"),
16#4B = Crc:Crc_CalculateCRC8(Ptr,9,16#FF,1).
```

The first assignment in this Erlang program binds the variable Ptr to the value of the C pointer in which the array of bytes is stored. The second assignment is an assertion only succeeding if indeed the called function returns the hexadecimal value 4B

In this test case, we use both the initial value and we supply the fact that we compute the CRC-result in a single call. If the last argument of this function is TRUE, then the function should always start from the initial value, ignoring Crc_StartValue8. In other words, the same test should hold for any 8 bit value of Crc_StartValue8. This is where QuickCheck comes in. We can write a property over arbitrary values:

```prop check() ->
?FORALL(Crc_StartValue8, byte(),
begin
Ptr = eqc_c:create_array("uint8","123456789"),
16#4B == Crc:Crc_CalculateCRC8(Ptr,9,Crc_StartValue8,1)
end).
```

A QuickCheck property is represented as an Erlang macro ?FORALL with three arguments. This corresponds to logical quantification with the second argument the domain of the quantification, in this case byte(). The generator byte() is a QuickCheck data generator that during testing will generate random values from 0 to 255. This generated value is bound to the first argument of the ?FORALLmacro, the binding variable Crc_StartValue8. The third and last argument is a logical statement in which the randomly generated value is used. Note that instead of the assertion Erlang’s equality operator (a double ==) is used. Running QuickCheck will result in hundred tests with a random value selected from the interval 0 to 255. Clearly, it would be possible to just check all possible values in this case, but in general enumerating all possible values for all parameters is impossible within reasonable time limits.

Now we would also like to vary the input data and send other blocks than the ASCII values from 1 to 9. However, if we were to do that, then we would need to know the outcome. Clearly the outcome is not always 4B! One could re-implement the function in Erlang and compare the Erlang result with the C function result. The disadvantages are that one has to implement the same function twice and that one can make the same mistake twice, therewith potentially not detecting a bug. Instead, we use the mathematical property Magic Check that can be performed independently of the data provided.

The AUTOSAR specification provides an example for Magic Check for the function CRC CalculateCRC8 as follows:

Magic check calculation of SAE-J1850 CRC8 over data bytes 00h 00h 00h 00h:

• CRC generation: CRC over 00h 00h 00h 00h, start value FFh:
CRC-result = 59h
• CRC check: CRC over 00h 00h 00h 00h 59h, start value FFh:
CRC-result = 3Bh
• Magic check = CRC-result XORed with XOR value:
C4h = 3Bh xor FFh

That is, for each data array, we compute the checksum, add the checksum to the data and compute the checksum over this extended array. After that, the checksum is XOR-ed with 0xFF and the outcome should then be 0xC4 irrespective of the initial data.

In order to write a QuickCheck property for this, we use a generator for arbitrary sequences of data list(byte()). We represent an array in Erlang as a list of bytes and use the append operator ++ to add an element to the end of the list. Finally we use Erlang’s build in operator for XOR on numbers, called bxor (the xor operator is reserved for boolean values).

```prop_magic_check() ->
?FORALL(Data, list(byte()),
begin
Ptr1 = eqc_c:create array("uint8",Data),
N    = length(Data),
Res1 = Crc:Crc_CalculateCRC8(Ptr1,N,16#FF,1),
Ptr2 = eqc_c:create_array("uint8",Data++[Res1]),
Res2 = Crc:Crc_CalculateCRC8(Ptr2,N+1,16#FF,1),
16#C4 == Res2 bxor 16#FF
end)).
```

With this property we test for arbitrary blocks of data. Clearly, it gets rather quickly impossible to enumerate all these values. It would take far too long to check all data blocks up to 10 bytes which each byte having 256 different values. Randomly selecting arbitrarily large blocks of data turns out to be very effective in detecting errors.

by 