FreeRTOS Case Study

In our second case study, the objetive was to evaluate the tool we developed using specifications for the FreeRTOS micro kernel. FreeRTOS provides a layer of abstraction for developers to access hardware features on real time systems. In this case study we have focused on the Queue modelue of the system which is responsible for controlling its message queues.

A simplified specification of the Queue module can be found here. You can download the generated test reports clicking here.

On the table below we present an overview of the generated test cases:

q_queueCreate 2 0 4 0 4 0
q_queueDelete 2 0 32 12 7 2
q_sendItem 2 1 64 12 7 1
q_receivedItem 2 1 4 3 4 3

During the case study we have faced some problems related to infeasible test cases. An infeasible test case happens when we combine two blocks which require a scenario that is impossible to happen (e.g. x > 10 and x < 0). We noticed this usually happened due to combination of multiple negative blocks.

To reduce this kind of scenarios we now generate negative blocks only for precondition and conditional characteristics and do not generate negative blocks for invariant characteristics. There is still a high number of test cases lost due to infeasibility as can be easily seen on the presented table. We have to refine our combination algorithms to reduce this scenarios even more.