Improving Reliability of Myocontrol Using Formal Verification

In the context of assistive robotics, myocontrol is one of the so-far unsolved problems of upper-limb prosthetics. It consists of swiftly, naturally, and reliably converting biosignals, non-invasively gathered from an upper-limb disabled subject, into control commands for an appropriate self-powered prosthetic device. Despite decades of research, traditional surface electromyography cannot yet detect the subject's intent to an acceptable degree of reliability, that is, enforce an action exactly when the subject wants it to be enforced. In this paper, we tackle one such kind of mismatch between the subject's intent and the response by the myocontrol system, and show that formal verification can indeed be used to mitigate it. Eighteen intact subjects were engaged in two target achievement control tests in which a standard myocontrol system was compared to two 'repaired' ones, one based on a non-formal technique, thus enforcing no guarantee of safety, and the other using the satisfiability modulo theories (SMT) technology to rigorously enforce the desired property. The experimental results indicate that both repaired systems exhibit better reliability than the non-repaired one. The SMT-based system causes only a modest increase in the required computational resources with respect to the non-formal technique; as opposed to this, the non-formal technique can be easily implemented in existing myocontrol systems, potentially increasing their reliability.