Safety considerations

Safety is a big issue with this project, if something goes wrong there's the potential for damage to building and serious injury to persons. The magnitude of a safety issue is its hazard, traditionally defined as the product of its probability (of happening at any point) and the (potential) consequence. Hazard = probability * consequence where all values are qualitative and arbitrary.

Concerns are split into the following categories: Issues we have solutions for, issues with a hazard great enough to warrant some form of mitigation and other miscellaneous hazards.

On top of all of this there are aspects of our implementation and guidelines for use which are there to minimise harm in any event. These are a hard-coded speed limit on the motor driver and the requirement that there is always a person in the driver's seat ready to cut power to the motor.

Safety Issue	Solution
Main battery power loss	Brownout detector on student board that pulls SD as high as possible.
Total CAN Bus failure	Detected on all nodes, kart stopped safely.

Safety Issue	Probability	Consequence	Mitigation
Linear actuator or brake controller fails	medium	high	Error condition detected by brake board, motor board moves into error state and slows engine down to minimum speed attainable through regenerative braking
Steering motor or controller board fails	medium	low	Same as above however error state on brake board will mean the kart can stop in even less time.
Software error causes board to stop responding	low	medium	Detected as error condition, all other boards transition to error state.
Moisture damage electronics	v. low	medium	N/A
Inherited safety issues	?	?	?

Formal Verification

Although simple in design, mistakes in the top level software had the potential to cause the most harm (ie a runaway kart) and was therefore subjected to heavy scrutiny. The formal verification system for distributed systems such as Mariokart called SPIN was used to prove the validity of an abstract model of the client server system.

Two models of the software were created. The first simply replicates state transitions and message passing. It's value is limited to an aid in design as it does not detect any issues that would not be found during testing.

The second model is slightly more involved. Instead of going to the complexity of modelling the CAN bus, it treats the message passing system as though it always works and allows boards to non-deterministically reset and transition to error state. The aim of this model is to prove that, regardless of failure mode (ie which board(s) fail/lose power), the states of all boards maintain their consistency. This constraint effectively sums up the approach the Mariokart system takes to safety. Failure is not necessarily prevented as this is not always a possibility, but it is always detected and always handled as gracefully as possible.