RTEMS SMP Formal

This repository contains the models and tooling developed as part of the ESA-sponsored activity Qualification of RTEMS Symmetric Multiprocessing (SMP), as well as result of ongoing contributions by students at Trinity College Dublin to improve and extend them.

Contributors

• Andrew Butterfield
• Frédéric Tuong
• Robert Jennings
• Jerzy Jaśkuć
• Eoin Lynch
• James Gooding Hunt
• Paddy Flanagan

License

This project is licensed under the BSD-2-Clause or CC-BY-SA-4.0.

Contents

• formal contains the formal models and python scripts to process them that are currently part of, or soon to be added to rtems-central.
• proto contains extra ideas developed during the ESA activity that may get introduced at some later stage.
• patch-sets hold patches that capture recent issues that have arisen while trying to sycnhronise between our work and foxes being done in the RTEMS repos.