RTEMS (https://www.rtems.org/) is an open-source real-time operating system widely used in aircraft and spacecraft. It offers a comprehensive API, mostly defined in terms of “managers” that provide calls to perform specific kinds of services or provide specific infrastructure.
As part of an activity sponsored by the European Space Agency (ESA) we have developed a methodology that used Promela/SPIN to model these managers, and to use them to automatically generate tests. We have applied this technique to a number of such managers. The results of this ESA activity are being fed back into the RTEMS open-source repository.
There are a number of different specific kinds of projects available:
- Generate models and tests of other RTEMS managers
- To complete existing partial models
- To refactor and rationalise the entire set of models and tests, by identifying commonalities and redundnacies.
Such projects can be done at both Year 4 and Year 5 levels. Year 5 would have some research element, such as comparing tests generated via Promela/SPIN with those generated by the specification system now used in RTEMS.
It would be expected that the results of these projects would also be fed back into RTEMS. The ESA work focussed on the so-called “Classic API” (https://docs.rtems.org/branches/master/c-user/index.html), but there is also scope to look at the more recent POSIX API (https://docs.rtems.org/branches/master/posix-users/index.html). For example, the POSIX API for RTEMS includes a pthreads library.