Apply Runtime Verification in a software using FreeRTOS

hamaral wrote on Saturday, December 01, 2018:


I’m working in a project that has developed (a long time ago) a control flight software using FreeRTOS (V7.5.2). We are using STM32F4discovery to embed the code and make analysis.

Now I want to apply runtime verification to check the execution and I found a toolchain that synthesize monitors and it uses a runtime library called RTMLib to take events from the main code.

However this RTMLib was developed for an RTOS that uses POSIX and is not the case of FreeRTOS. So, what I should to do is to modify any files to adapt it to FreeRTOS. In the case this is the header:

I read FreeRTOS APIs and others documents, but as I’m new in RTOS and I don’t know what function can replace "pthread_attr " in this file .

Could anyone help me, please?

rtel wrote on Saturday, December 01, 2018:

This page
includes a download link that contains a pre-release version of
FreeRTOS+POSIX - a new POSIX threading wrapper for the FreeRTOS kernel
provided by AWS - does that help you?

hamaral wrote on Saturday, December 01, 2018:

Thanks to the answer Richard.

As I understood, I will need to modify and adapt the original code that uses the FreeRTOS API to this one, or I can add this wrapper into my FreeRTOS folder (which it has all headers and auxiliary structures), maintain my original code and uses this POSIX API to link with the RTMLib library.

In this case, I will need to modify also my port.c file (I’m using the GCC/ARM_CM4F)?

rtel wrote on Sunday, December 02, 2018:

If you include the FreeRTOS+POSIX library in your project then your
existing code can continue to use the native FreeRTOS kernel API and the
library code can use the pthread API.