a As for the priority inversion avoidance test, both NuttX > and ChibiOS passed. However, with NuttX, we found that > there is no priority inheritance implemented for threads > blocked on a mutex but only on a binary semaphore. >
This is completely untrue. Certainly priority inheritance is supported on pthread mutexes (provided that you enable that option using the standard POSIX interfaces. In NuttX, pthread mutexes are designed on top of binary semaphores so any feature supported by binary semaphores is also supported by pthread mutexes.