Post-doctoral researcher
Rigorous System Design Laboratory
EPFL, Lausanne, Switzerland

 

Webpage

Formal Approaches to Safe Software Development for Medical Devices

Friday, 11 December 2015 at 11:00 in room BC 420

 

Abstract:

Recently, the set of electronic medical devices has a tendency to be extended with a new class of closed-loop/autonomous devices able to not only acquire the vital information but also perform some basic patient treatment. Medical Guidelines (GLs) contain step-by-step recommendations for practitioners about how to treat a patient. Therefore, they represent an informal control flow that synchronizes the processes of data acquisition, decision-making and treatment provision and thus playing a role of a medical system specification.

Until now, most of the GLs are represented in a textual format and often suffer from such structural problems as incompleteness, inconsistency, ambiguity and redundancy. Therefore, it is essential to find a proper representation for the GLs that would enable the validation of the GLs formal properties. It is also important to choose one of the standard techniques for the development of safety-critical embedded software, which would allow the reuse of the GL models when building the software for medical devices.

During the talk I will show that a well-known formal behavior representation approach of embedded systems design domain that employs Timed Automaton extended with Tasks (TAT) can be used to represent medical GLs. I will show how TAT is used to formalize not only action-based step-by-step procedures of a medical GL but also a response to the treatment definition by means of response level observers. As a case study I will use the dose adjustment for adult patients part of the protocol for anticancer drug called imatinib. The drug is used to treat patients  with newly diagnosed Philadelphia positive (Ph+) Chronic Myeloid Leukemia (CML).

I will also present a complementary TAT-based models of an observers guarding the defined response levels and the ’rescue’ TDM approach for efficacy and tolerance concerns that enhance the model without contradicting official protocol for patients treatment with imatinib. I will show that we were able to fix some incompleteness problems in these models.

 

 

About the speaker:

Alena Simalatsar received her PhD in Computer Science and Telecommunication Technologies in 2009 from the University of Trento, Italy, where she focused on system-level analysis methodologies for embedded systems. During her PhD studies she spent six months as a Visiting Scholar at the Department of Electrical Engineering and Computer Sciences of the University of California at Berkeley, USA. She received her Bachelor and her masters degree from the Faculty of Radiophysics and Computer Technologies of Belarusian State University in 2005. Her master thesis was dedicated to the development of a closed-loop controller for a cyber-physical system, a vacuum thin-film deposition chamber.

Dr. Simalatsar is currently working as a postdoctoral researcher at Ecole Polytechnique Fédéral de Lausanne (EPFL), Switzerland. Her current work and interest is focused on safety and reliability analysis of medical devices including the critical health care closed-loop/autonomous devices, such as autonomous drug delivery systems, and medical ultrasound systems.