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.
Unlike the Promela/SPIN related projects, there is no pre-exisitng infrastructure so this project is aimed at year 5 dissertation level.