Dependability Case for Surgical Robots

Safety-critical applications often use dependability cases to validate that specified properties are invariant, or to demonstrate a counterexample showing how that property might be violated. Most dependability cases are written with a single product in mind, but in this study, we construct a dependability case for a surgery robot system built for a family of robots. We have brought together lightweight formal analysis, feature modeling, and testing in our approach to investigating if a safety-critical property is violated.

The following diagram shows the overall process of building the dependability case.

The safety critical property we are checking in the system with this approach is as follows:

Arm movement safety property: During the surgery procedure, as the surgeon moves the control device, the actual position of the robot arm should be the same position that the surgeon articulates in the control workspace, and he/she should be notified if the arm is pushed outside of its physical range.

The feature model is developed using FeatureIDE, a tool that supports all phases of feature-oriented software development for the development of Software Products Lines. The formal model is developed in Alloy, a lightweight formal specification language based on first-order relational logic, with an analysis engine that performs verification of models in a specific scope. We use the analyzer for checking an assertion that defines the safety-critical property, and the analyzer is capable of generating counterexamples to show a scenario where the property is violated.

Feature Model

Clicking on the image below that shows the partial feature model for the surgery robot system will lead you to the complete, full-size version. The XML file can also be downloaded here.

You can also see the list of constraints defined in the Feature model in this page. These constraints are enforced in the system, and by imposing these constraints on our model, we make sure that all the products created by FeatureIDE are valid.

Alloy Model

The Alloy meta-model is used to describe components of the system and the relationship between them. We can use the Alloy Analyzer to check the critical safety property automatically. The meta-model and the individual robot models are available for download here.

As an example, the FrankenVREP robot arm is one of the individual robot models. The Alloy analyzer gives us a counterexample of the assertion, which means that the Arm Movement property can be violated when using this robot arm. The relevant part of the counterexample is seen in the figure below.