Bristol University (Bristol, UK)
Verified Robot Control Software
At the University of Bristol and at the Bristol Robotics Laboratory we want to trust our robots. We develop their control software in Ada/SPARK and verify it using the latest technology from AdaCore. Within the RIVERAS project (Robust Integrated Verification of Autonomous Systems) we aim to create systems that behave predictable even in the face of unpredicted events.
Ada is a perfect choice for the development of robot control software, where the programming challenges of embedded, real-time and distributed systems occur all at once. Depending on the context, we rely on different features of Ada and use different AdaCore tools.
We implement the low-layer control algorithms in SPARK and verify that they are free from run-time errors with GNATProve. For the tasking code we use the Ravenscar Profile, which guarantees that the real-time behaviour of our robots is deterministic. If the robots need to talk to each other, we use the Distributed Systems Annex of Ada and the PolyORB middleware.