Modeling and testing a family of surgical robots: An experience report

Niloofar Mansoor, Jonathan A. Saddler, Bruno Silva, Hamid Bagheri, Myra B. Cohen, Shane Farritor

Research output: Chapter in Book/Report/Conference proceedingConference contribution

1 Citation (Scopus)

Abstract

Safety-critical applications often use dependability cases to validate that specified properties are invariant, or to demonstrate a counter example showing how that property might be violated. However, most dependability cases are written with a single product in mind. At the same time, software product lines (families of related software products) have been studied with the goal of modeling variability and commonality, and building family based techniques for both analysis and testing. However, there has been little work on building an end to end dependability case for a software product line (where a property is modeled, a counter example is found and then validated as a true positive via testing), and none that we know of in an emerging safety-critical domain, that of robotic surgery. In this paper, we study a family of surgical robots, that combine hardware and software, and are highly configurable, representing over 1300 unique robots. At the same time, they are considered safety-critical and should have associated dependability cases. We perform a case study to understand how we can bring together lightweight formal analysis, feature modeling, and testing to provide an end to end pipeline to find potential violations of important safety properties. In the process, we learned that there are some interesting and open challenges for the research community, which if solved will lead towards more dependable safety-critical cyber-physical systems.

Original languageEnglish (US)
Title of host publicationESEC/FSE 2018 - Proceedings of the 2018 26th ACM Joint Meeting on European So ftware Engineering Conference and Symposium on the Foundations of So ftware Engineering
EditorsAlessandro Garci, Corina S. Pasareanu, Gary T. Leavens
PublisherAssociation for Computing Machinery, Inc
Pages785-790
Number of pages6
ISBN (Electronic)9781450355735
DOIs
StatePublished - Oct 26 2018
Event26th ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering, ESEC/FSE 2018 - Lake Buena Vista, United States
Duration: Nov 4 2018Nov 9 2018

Publication series

NameESEC/FSE 2018 - Proceedings of the 2018 26th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering

Other

Other26th ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering, ESEC/FSE 2018
CountryUnited States
CityLake Buena Vista
Period11/4/1811/9/18

Fingerprint

Testing
Pipelines
Robotic surgery
Robots
Hardware
Cyber Physical System

Keywords

  • Alloy
  • cyber-physical systems
  • software product lines
  • testing and analysis

ASJC Scopus subject areas

  • Software
  • Artificial Intelligence

Cite this

Mansoor, N., Saddler, J. A., Silva, B., Bagheri, H., Cohen, M. B., & Farritor, S. (2018). Modeling and testing a family of surgical robots: An experience report. In A. Garci, C. S. Pasareanu, & G. T. Leavens (Eds.), ESEC/FSE 2018 - Proceedings of the 2018 26th ACM Joint Meeting on European So ftware Engineering Conference and Symposium on the Foundations of So ftware Engineering (pp. 785-790). (ESEC/FSE 2018 - Proceedings of the 2018 26th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering). Association for Computing Machinery, Inc. https://doi.org/10.1145/3236024.3275534

Modeling and testing a family of surgical robots : An experience report. / Mansoor, Niloofar; Saddler, Jonathan A.; Silva, Bruno; Bagheri, Hamid; Cohen, Myra B.; Farritor, Shane.

ESEC/FSE 2018 - Proceedings of the 2018 26th ACM Joint Meeting on European So ftware Engineering Conference and Symposium on the Foundations of So ftware Engineering. ed. / Alessandro Garci; Corina S. Pasareanu; Gary T. Leavens. Association for Computing Machinery, Inc, 2018. p. 785-790 (ESEC/FSE 2018 - Proceedings of the 2018 26th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Mansoor, N, Saddler, JA, Silva, B, Bagheri, H, Cohen, MB & Farritor, S 2018, Modeling and testing a family of surgical robots: An experience report. in A Garci, CS Pasareanu & GT Leavens (eds), ESEC/FSE 2018 - Proceedings of the 2018 26th ACM Joint Meeting on European So ftware Engineering Conference and Symposium on the Foundations of So ftware Engineering. ESEC/FSE 2018 - Proceedings of the 2018 26th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering, Association for Computing Machinery, Inc, pp. 785-790, 26th ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering, ESEC/FSE 2018, Lake Buena Vista, United States, 11/4/18. https://doi.org/10.1145/3236024.3275534
Mansoor N, Saddler JA, Silva B, Bagheri H, Cohen MB, Farritor S. Modeling and testing a family of surgical robots: An experience report. In Garci A, Pasareanu CS, Leavens GT, editors, ESEC/FSE 2018 - Proceedings of the 2018 26th ACM Joint Meeting on European So ftware Engineering Conference and Symposium on the Foundations of So ftware Engineering. Association for Computing Machinery, Inc. 2018. p. 785-790. (ESEC/FSE 2018 - Proceedings of the 2018 26th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering). https://doi.org/10.1145/3236024.3275534
Mansoor, Niloofar ; Saddler, Jonathan A. ; Silva, Bruno ; Bagheri, Hamid ; Cohen, Myra B. ; Farritor, Shane. / Modeling and testing a family of surgical robots : An experience report. ESEC/FSE 2018 - Proceedings of the 2018 26th ACM Joint Meeting on European So ftware Engineering Conference and Symposium on the Foundations of So ftware Engineering. editor / Alessandro Garci ; Corina S. Pasareanu ; Gary T. Leavens. Association for Computing Machinery, Inc, 2018. pp. 785-790 (ESEC/FSE 2018 - Proceedings of the 2018 26th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering).
@inproceedings{1d16c8d2541c4dbba09f4f8f5bb01daa,
title = "Modeling and testing a family of surgical robots: An experience report",
abstract = "Safety-critical applications often use dependability cases to validate that specified properties are invariant, or to demonstrate a counter example showing how that property might be violated. However, most dependability cases are written with a single product in mind. At the same time, software product lines (families of related software products) have been studied with the goal of modeling variability and commonality, and building family based techniques for both analysis and testing. However, there has been little work on building an end to end dependability case for a software product line (where a property is modeled, a counter example is found and then validated as a true positive via testing), and none that we know of in an emerging safety-critical domain, that of robotic surgery. In this paper, we study a family of surgical robots, that combine hardware and software, and are highly configurable, representing over 1300 unique robots. At the same time, they are considered safety-critical and should have associated dependability cases. We perform a case study to understand how we can bring together lightweight formal analysis, feature modeling, and testing to provide an end to end pipeline to find potential violations of important safety properties. In the process, we learned that there are some interesting and open challenges for the research community, which if solved will lead towards more dependable safety-critical cyber-physical systems.",
keywords = "Alloy, cyber-physical systems, software product lines, testing and analysis",
author = "Niloofar Mansoor and Saddler, {Jonathan A.} and Bruno Silva and Hamid Bagheri and Cohen, {Myra B.} and Shane Farritor",
year = "2018",
month = "10",
day = "26",
doi = "10.1145/3236024.3275534",
language = "English (US)",
series = "ESEC/FSE 2018 - Proceedings of the 2018 26th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering",
publisher = "Association for Computing Machinery, Inc",
pages = "785--790",
editor = "Alessandro Garci and Pasareanu, {Corina S.} and Leavens, {Gary T.}",
booktitle = "ESEC/FSE 2018 - Proceedings of the 2018 26th ACM Joint Meeting on European So ftware Engineering Conference and Symposium on the Foundations of So ftware Engineering",

}

TY - GEN

T1 - Modeling and testing a family of surgical robots

T2 - An experience report

AU - Mansoor, Niloofar

AU - Saddler, Jonathan A.

AU - Silva, Bruno

AU - Bagheri, Hamid

AU - Cohen, Myra B.

AU - Farritor, Shane

PY - 2018/10/26

Y1 - 2018/10/26

N2 - Safety-critical applications often use dependability cases to validate that specified properties are invariant, or to demonstrate a counter example showing how that property might be violated. However, most dependability cases are written with a single product in mind. At the same time, software product lines (families of related software products) have been studied with the goal of modeling variability and commonality, and building family based techniques for both analysis and testing. However, there has been little work on building an end to end dependability case for a software product line (where a property is modeled, a counter example is found and then validated as a true positive via testing), and none that we know of in an emerging safety-critical domain, that of robotic surgery. In this paper, we study a family of surgical robots, that combine hardware and software, and are highly configurable, representing over 1300 unique robots. At the same time, they are considered safety-critical and should have associated dependability cases. We perform a case study to understand how we can bring together lightweight formal analysis, feature modeling, and testing to provide an end to end pipeline to find potential violations of important safety properties. In the process, we learned that there are some interesting and open challenges for the research community, which if solved will lead towards more dependable safety-critical cyber-physical systems.

AB - Safety-critical applications often use dependability cases to validate that specified properties are invariant, or to demonstrate a counter example showing how that property might be violated. However, most dependability cases are written with a single product in mind. At the same time, software product lines (families of related software products) have been studied with the goal of modeling variability and commonality, and building family based techniques for both analysis and testing. However, there has been little work on building an end to end dependability case for a software product line (where a property is modeled, a counter example is found and then validated as a true positive via testing), and none that we know of in an emerging safety-critical domain, that of robotic surgery. In this paper, we study a family of surgical robots, that combine hardware and software, and are highly configurable, representing over 1300 unique robots. At the same time, they are considered safety-critical and should have associated dependability cases. We perform a case study to understand how we can bring together lightweight formal analysis, feature modeling, and testing to provide an end to end pipeline to find potential violations of important safety properties. In the process, we learned that there are some interesting and open challenges for the research community, which if solved will lead towards more dependable safety-critical cyber-physical systems.

KW - Alloy

KW - cyber-physical systems

KW - software product lines

KW - testing and analysis

UR - http://www.scopus.com/inward/record.url?scp=85058276845&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=85058276845&partnerID=8YFLogxK

U2 - 10.1145/3236024.3275534

DO - 10.1145/3236024.3275534

M3 - Conference contribution

AN - SCOPUS:85058276845

T3 - ESEC/FSE 2018 - Proceedings of the 2018 26th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering

SP - 785

EP - 790

BT - ESEC/FSE 2018 - Proceedings of the 2018 26th ACM Joint Meeting on European So ftware Engineering Conference and Symposium on the Foundations of So ftware Engineering

A2 - Garci, Alessandro

A2 - Pasareanu, Corina S.

A2 - Leavens, Gary T.

PB - Association for Computing Machinery, Inc

ER -