Cubesats are small satellites that are built as on ore more 10cm-sized cubes. There is a growing industry for developing and launching these. Typically their computing requirements are relatively low, and so they often use lightweight versions of operating systems. This project looks at using Promela/SPIN to model and do test generation for some key features of an operating system currently being developed for cubesat use.
A dissertation project in 2024-25 has made a first cut at setting up the modelling and test generation infrastructure, by modelling a simple scenario involving task managment API calls.
There is now scope to work on (i) modelling features other than task management, and (ii) improving the exisiting infrastructure to support more comprehensive testing of tasks. This can be scoped for Year 4 or year 5.
The work involves a company with whom TCD has signed an NDA, but the projects can be scoped to stay in the public domain.