Robot-assisted dressing

Trustworthy Autonomous Systems Robot-Assisted Dressing Case Study

Patients with limited physical mobility frequently require assistance in daily living tasks such as getting dressed. Whilst this assistance is typically provided by human caregivers, a combination of ageing populations and a shortage of caregivers, motivates the development of robotic assistants to supplement the supply of human caregivers. Additionally, robotic assistance has the potential to increase the independence and privacy of patients, by allowing them to perform a wider ranger of tasks without the involvement of professional or informal caregivers.

This case study involves a robotic assistant of aiding patients with limited upper limb mobility (such as many stroke survivors) in getting dressed. Specifically, we look at the use of a robotic arm to perform a jacket dressing task, where the robotic arm picks up one arm of a jacket, moves this over the impaired arm of the user, and then places the garment appropriately to allow the user to complete the dressing task with their unimpaired arm.

The modelling and verification aspects of this case study were carried out as part of the Trustworthy Autonomous Systems (TAS) Verifiability Node, whilst a physical version of the dressing robot was carried in Sheffield as part of the TAS Resilience Node.

Robotic Platform

The robotic platform consists of a 7 Degrees-of-Freedom (DoF) Franka-Emika robotic arm. This is augmented with a gripper device and a force sensor used to detect the force vector at the end of the gripper. The pose of the user is detected using a RGB-D camera, this the robot communicates with the user via voice commands.

Dressing Flow and Sensors

The following diagram (adapted from [5]) shows the main control flow for the dressing process including how each of the different sensors is used during the dressing process. RAD Control Flow

Robot Arm Model

We modelled the Franka-Emika arm at the centre of this case study as a RoboSim p-model. This has the following structure, including the kinematic chain making up the 7oF arm, as well as the end effector, alongside each of the actuators of the arm and the end-effector force sensor.

This was used to generate a SDF file for the arm, which can be realised as a 3D model for visualisation and simulation in standard robotics such as CoppeliaSim and Gazebo. Arm SDF model

Dressing Controller

We modelled the central dressing controller driving the dressing process in RoboChart. We split this into two versions with differing level of detail, as a means to apply different types of verification to the case study.

Dressing Controller: Simple Model

Firstly, we have a simple model, which just contains just a single state machine corresponding to the core dressing flow of the robot. Dressing Controller Simple This treats the movement of the robot at a rather high-level, with movement started by movementStart and forceStart events which are assumed to be provided by the robotic platform to perform position control or force control to move towards as desired target attention, coupled with corresponding movementStop and forceStop events marking when the movement has been concluded.

Dressing Controller: Full Model

We also have a much more complex version of the model which combines several state machines in addition to the core dressing flow modelling different aspects of the dressing controller.

The following diagram shows the overall structure of the controller: Full Dressing controller model

This consists of the following components.

Core Dressing Control

The SDressingControl state machine is the same as the simple model, except the movement events are implemented in the other modules of the controller rather than provided directly from the movement platform, and additional checkHRI and allowHRI events are used to block the dressing process at certain points. Full Dresssing Control State Machine

Movement Control and PID

The MovementControl implements the actual movement of the robot arm end effector to a given point. It has two modes:

Position Control: directly control the position of the end effector to move towards the desired target. This is used when the robot arm is moving in free space.
Force Control: control the force applied at the end effector to move towards the desired target, using the force sensor at the end effector.

Both of these are implement as PID feedback loops using the following operations which implements a reusable PID feedback loop.

Stop Control and Environmental Monitor

The StopControl state machine keeps track of whether the dressing controller is currently allowed to progress, or is in a stopped state. This is used to implement a safe stop, in which the robot arm is placed into a compliant mode, in which it makes no movement, but allows for user movement (for example, when the user’s arm is still inserted into a gripped garment).

This handles stops occurring in the following scenarios:

User stop requests
Collisions
Environmental stops

Environmental stops are handled separately in the EnvironmentalMonitor state machine and occur either:

When the user leaves the dressing area
When background noise is too high to rely on voice communication
When other people enter the dressing area

Analysis

RoboSim translation

This case study served as a test case for the automatic translation between RoboChart and RoboSim, producing a RoboSim d-model.

RoboCert Specification and Verification

We used the RoboCert specification language to specify a number of properties of the simple dressing controller:

specification group RAD {

    target = module RADnew_RobotAssistedDressingIsolated

    // 1. 
    // [High severity hazard]
    // Property: Ensure forceStart only happens after user has confirmed they are ready and when a valid pose is detected
    sequence ForceStartAfterConfirmationAndPoseDetection {
        actors System and Environment

        // Initial dressing request and user confirmation
        any except {Environment->>System: event dressingRequest} until
            Environment->>System: event dressingRequest
            System->>Environment: op RADnew_checkUserReady()
            any except {Environment->>System: event userConfirmsReady(true)} until
                Environment->>System: event userConfirmsReady(true)
            end
        end

        // Garment detection and handling
        System->>Environment: op RADnew_detectGarment()
        any except {Environment->>System: event garmentDetected(any)} until
            Environment->>System: event garmentDetected(any)
            System->>Environment: event movementStart(any)
            any except {Environment->>System: event movementEnd} until
                Environment->>System: event movementEnd
                System->>Environment: op RADnew_grip()
                any except {Environment->>System: event gripperEngaged(true), Environment->>System: event gripperEngaged(false)} until
                    Environment->>System: event gripperEngaged(true)
                    System->>Environment: event garmentGripped
                    System->>Environment: op RADnew_checkCorrectHandling()
                    any except {Environment->>System: event handlingCorrect(true), Environment->>System: event handlingCorrect(false)} until
                        Environment->>System: event handlingCorrect(true)
                    end
                end
            end
        end

        // Valid pose detection
        System->>Environment: op RADnew_detectUserPose()
        any except {Environment->>System: event invalidPoseDetected} until
            Environment->>System: event poseDetected(any)
            System->>Environment: event forceStart(any)
            any until
                deadlock (on System)
            end
        end
    }



    // 2. 
    // [annoyance]
    // Safety Property: Ensure system transitions to GarmentToUser only after the garment is gripped and user confirms ready
    sequence GarmentToUserSafety {
        actors System and Environment

        // Initial Events: The environment sends a dressing request to the system
        Environment->>System: event dressingRequest

        // The system checks if the user is ready
        System->>Environment: op RADnew_checkUserReady()
        any except {Environment->>System: event userConfirmsReady(true)} until
            Environment->>System: event userConfirmsReady(true)
        end
        
        // The system performs the detectGarment() operation
        System->>Environment: op RADnew_detectGarment()      

        // The environment sends garmentDetected event to the system with any parameter
        Environment->>System: event garmentDetected(any)     

        // The system sends a 'movementStart' event to the environment with any parameter
        System->>Environment: event movementStart(any)       

        any except {Environment->>System: event movementEnd} until
            Environment->>System: event movementEnd
        end
        
        // Ensure the garment is gripped correctly
        any except grippingEvents until
            opt 
                Environment->>System: event gripperEngaged(true)
                System->>Environment: event garmentGripped
            end
            opt 
                Environment->>System: event gripperEngaged(false)
                System->>Environment: op RADnew_detectGarment()
            end
            opt 
                Environment->>System: event gripTimeoutHRI
            end
        end

        // The property holds until a deadlock occurs on the system
        any until 
            deadlock (on System)
        end
    }

    message set grippingEvents = {
        Environment->>System: event gripperEngaged(true),
        Environment->>System: event gripperEngaged(false),
        Environment->>System: event gripTimeoutHRI
    }
    
    
    // 3. 
    // [High severity hazard]
    // Safety Property: Ensure robot movement does not continue after dressing is complete [High severity hazard]
    sequence NoMovementAfterDressed2 {
        actors System and Environment
        any until
            Environment->>System: event userDressed  
            any except {System->>Environment: event movementStart(any), Environment->>System: event movementEnd} until
                deadlock (on System)
            end
        end
    }


    // 4. 
    // [low risk]
    // Safety Property: Ensure garment is not picked up without dressingRequest event 
    sequence NoGarmentPickupWithoutRequest {
        actors System and Environment
        any except {Environment->>System: event dressingRequest} until
            Environment->>System: event dressingRequest
            any except {System->>Environment: event garmentGripped} until
                System->>Environment: event garmentGripped
                any until
                    deadlock (on System)
                end
            end
        end
    }

    // 5. 
    // [High severity hazard]
    // Sequence to ensure the joints are dressed in the correct order: 2, 1, 0, valid dressing trajectory
    sequence DressesInOrder2 {
        actors System and Environment
        any except MJoints2 until
            System->>Environment: event dressedJoint(2)
        end
        any except MJoints2 until
            System->>Environment: event dressedJoint(1)
        end
        any except MJoints2 until
            System->>Environment: event dressedJoint(0)
        end
        any until
            deadlock (on System)
        end
    }
    
    
    // 6. 
    // [High severity hazard]
    // Property to ensure joints are dressed in the correct order
    sequence DressesIncorrectOrder {
        actors System and Environment
        any except MJoints2 until
            System->>Environment: event dressedJoint(1) end
            any except MJoints2 until
            System->>Environment: event dressedJoint(2) end
            any except MJoints2 until
            System->>Environment: event dressedJoint(0) end
            any until
                deadlock (on System)
       end
    }

    message set MJoints2 = {
        System->>Environment: event dressedJoint(0),
        System->>Environment: event dressedJoint(1),
        System->>Environment: event dressedJoint(2)
    }


    // 7. 
    // [High severity hazard]
    // Safety Property: Ensure robot always goes to SnaggingCorrection on snagging detection
    sequence SnaggingDetectionSafety {
        actors System and Environment
        loop
            any until 
                Environment->>System: event forceEnd(CompletionStatus::SnaggingDetected)
                System->>Environment: event correctedMovement
            end
        end
        any until
            deadlock (on System)
        end
    }
    
    

    
    
    // 8. 
    // [Annoyance]
    // Safety Property: Ensure dressing request only starts after user confirms ready
    sequence DressingRequestAfterUserConfirmation {
        actors System and Environment

        // Initial state, waiting for dressing request
        any except {Environment->>System: event dressingRequest} until
            Environment->>System: event dressingRequest
            System->>Environment: op RADnew_checkUserReady()

            // Ensure user confirms ready before starting dressing request
            loop
                any except {Environment->>System: event userConfirmsReady(true)} until
                    Environment->>System: event userConfirmsReady(true)
                end
                any except {System->>Environment: op RADnew_detectGarment()} until
                    System->>Environment: op RADnew_detectGarment()
                end
            end

            any until
                deadlock (on System)
            end
        end
    }
    
    
    // 9. 
    // [Low risk hazard]
    // Safety Property: Ensure robot finishes dressing after userDressed and then releases the grip
    sequence FinishDressingAfterUserDressed {
        actors System and Environment

        // Initial state, waiting for dressing request
        any except {Environment->>System: event userDressed} until
            Environment->>System: event userDressed

            // Ensure the robot releases the grip after userDressed
            System->>Environment: op RADnew_releaseGrip()
            
            any until
                deadlock (on System)
            end
        end
    }
    
    
    // 10.
    // [High severity hazard]
    // Property: Ensure SnaggingCorrection always happens when SnaggingDetected is detected
    sequence SnaggingCorrectionAfterDetection {
        actors System and Environment

        // Initial dressing request
        any except {Environment->>System: event dressingRequest} until
            Environment->>System: event dressingRequest

            // Detecting pose and starting force
            any except {System->>Environment: event forceStart(any)} until
                System->>Environment: event forceStart(any)
                
                // Ensure SnaggingCorrection happens when SnaggingDetected is detected
                any except {Environment->>System: event forceEnd(CompletionStatus::SnaggingDetected)} until
                    Environment->>System: event forceEnd(CompletionStatus::SnaggingDetected)
                    System->>Environment: event correctedMovement
                    any until
                        deadlock (on System)
                    end
                end
            end
        end
    }
 
 
    // 11. 
    // [Medium risk hazard]
    // Property: Ensure user pose is detected again if user moves (forceResult == CompletionStatus::InvalidPose)
    sequence DetectUserPoseAfterInvalidPose {
        actors System and Environment

        // Initial dressing request
        any except {Environment->>System: event dressingRequest} until
            Environment->>System: event dressingRequest

            // Detecting pose and starting force
            any except {System->>Environment: event forceStart(any)} until
                System->>Environment: event forceStart(any)
                
                // Ensure detectUserPose is called if forceResult == InvalidPose
                any except {Environment->>System: event forceEnd(CompletionStatus::InvalidPose)} until
                    Environment->>System: event forceEnd(CompletionStatus::InvalidPose)
                    System->>Environment: op RADnew_detectUserPose()
                    any until
                        deadlock (on System)
                    end
                end
            end
        end
    }
 
    // 12.
    // [Medium risk hazard]
    // Safety Property: Ensure forceEnd occurs within 1 tock after forceStart
    sequence ForceEndWithinTime {
        actors System and Environment

        // Initial dressing request and user confirmation
        any except {Environment->>System: event dressingRequest} until
            Environment->>System: event dressingRequest
            any except {System->>Environment: op RADnew_checkUserReady()} until
                System->>Environment: op RADnew_checkUserReady()
                any except {Environment->>System: event userConfirmsReady(true)} until
                    Environment->>System: event userConfirmsReady(true)
                end
            end
        end

        // Ensure garment is gripped and with the user
        any except {System->>Environment: event garmentGripped} until
            System->>Environment: event garmentGripped
        end
        any except {System->>Environment: event garmentAtHand} until
            System->>Environment: event garmentAtHand
        end

        // Detect user pose and start force
        any except {System->>Environment: event poseDetected(any)} until
            System->>Environment: event poseDetected(any)
            any except {System->>Environment: event forceStart(any)} until
                System->>Environment: event forceStart(any)

                // Ensure forceEnd occurs within 1 tock after forceStart
                deadline (1 on System)
                    alt
                        System->>Environment: event forceEnd(CompletionStatus::Success)
                    else
                        System->>Environment: event forceEnd(CompletionStatus::InvalidPose)
                    else
                        System->>Environment: event forceEnd(CompletionStatus::SnaggingDetected)
                    end
                end
            end
        end

        any until
            deadlock (on System)
        end
    }



    // 13. 
    // [High severity hazard]
    // Property: Ensure forceStart only happens after a valid pose is detected
    sequence ForceStartAfterPoseDetection {
        actors System and Environment

        // Initial dressing request
        any except {Environment->>System: event dressingRequest} until
            Environment->>System: event dressingRequest

            // No invalid poses should be detected
            any except {Environment->>System: event invalidPoseDetected} until

                // Force start should only happen after the above conditions are met
                System->>Environment: event forceStart(any)

                // Ensure no deadlock on the system
                any until
                    deadlock (on System)
                end
            end
        end
    }



    
    // Define actors
    actors = { target as System, world as Environment }
}

assertion GarmentToUserSafety: RAD::GarmentToUserSafety holds in the traces model
assertion NoGarmentPickupWithoutRequest: RAD::NoGarmentPickupWithoutRequest holds in the traces model
assertion ForceStartAfterPoseDetection: RAD::ForceStartAfterPoseDetection holds in the traces model
assertion NoMovementAfterDressed: RAD::NoMovementAfterDressed2 holds in the traces model
assertion DressesInOrder2: RAD::DressesInOrder2 holds in the traces model
assertion DressesOutOfOrder2: RAD::DressesIncorrectOrder is not observed in the traces model
assertion DressesOutOfOrder3: RAD::DressesIncorrectOrder does not hold in the traces model
assertion SnaggingCorrectionSafety: RAD::SnaggingDetectionSafety holds in the traces model
assertion DressingRequestAfterUserConfirmation: RAD::DressingRequestAfterUserConfirmation holds in the traces model
assertion FinishDressingAfterUserDressed: RAD::FinishDressingAfterUserDressed holds in the traces model
assertion SnaggingCorrectionAfterDetection: RAD::SnaggingCorrectionAfterDetection holds in the traces model
assertion DetectUserPoseAfterInvalidPose: RAD::DetectUserPoseAfterInvalidPose holds in the traces model
assertion ForceEndWithinTime: RAD::ForceEndWithinTime holds in the traces model

Each of these properties have been verified in the FDR4 model checker.

SDF representation of P-Model

The SDF file can be downloaded here

References

The Robot-Assisted Dressing case study itself builds on the following works:

Chance G, Jevtić A, Caleb-Solly P, Dogramadzi S. A quantitative analysis of dressing dynamics for robotic dressing assistance. Frontiers in Robotics and AI. 2017;4:13.
Chance G, Camilleri A, Winstone B, Caleb-Solly P, Dogramadzi S. An assistive robot to support dressing-strategies for planning and error handling. In: 2016 6th IEEE International Conference on Biomedical Robotics and Biomechatronics (BioRob). IEEE; 2016. p. 774–80.
Chance G, Jevtic A, Caleb-Solly P, Alenyà G, Torras C, Dogramadzi S. ‘Elbows Out’ - Predictive Tracking of Partially Occluded Pose for Robot-Assisted Dressing. IEEE Robotics Autom Lett. 2018;3(4):3598–605.
Dogramadzi S, Giannaccini ME, Harper C, Sobhani M, Woodman R, Choung J. Environmental hazard analysis-a variant of preliminary hazard analysis for autonomous mobile robots. Journal of Intelligent & Robotic Systems. 2014;76(1):73–117.

Frontiers

Safety Assessment Review of a Dressing Assistance Robot [Internet]. [cited 2023 May 5]. Available from: https://www.frontiersin.org/articles/10.3389/frobt.2021.667316/full

Jevtić A, Valle AF, Alenyà G, Chance G, Caleb-Solly P, Dogramadzi S, et al. Personalized robot assistant for support in dressing. IEEE transactions on cognitive and developmental systems. 2018;11(3):363–74.
Delgado Bellamy D, Chance G, Caleb-Solly P, Dogramadzi S. Safety Assessment Review of a Dressing Assistance Robot. Frontiers in Robotics and AI [Internet]. 2021 [cited 2023 May 5];8. Available from: https://www.frontiersin.org/articles/10.3389/frobt.2021.667316
Chance G, Caleb-Solly P, Jevtić A, Dogramadzi S. What’s “up”?—Resolving interaction ambiguity through non-visual cues for a robotic dressing assistant. In: 2017 26th IEEE international symposium on robot and human interactive communication (RO-MAN). IEEE; 2017. p. 284–91.