Model Checking – Student Projects

Using Promela/SPIN to verify lightweight operating systems for Cubesats

Andrew Butterfield (email | all projects)

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 … Read more

Using Promela/SPIN to verify RTEMS

Andrew Butterfield (email | all projects)

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 … Read more