Abstraction-Tree For Closed-loop Model Checking of Medical Devices

摘要: ion-Tree For Closed-loop Model Checking of Medical Devices Disciplines Computer Engineering | Electrical and This technical report is available at ScholarlyCommons: http://repository.upenn.edu/mlab_papers/73 Abstraction Trees for Closed-Loop Devicesion Zhihao Jiang, Houssam Abbas, Pieter J. Mosterman, Rahul Mangharam 1 Department Systems Engineering, University Pennsylvania 2 School Science, McGill University, Canada 3 MathWorks, USA Abstract. paper proposes a methodology closed-loop model checking medical devices, illustrates it with case study on implantable cardiac pacemakers. To evaluate the performance device human body, device’s physiological environment must be developed, consisting (e.g., pacemaker) heart) model-checked. Formal modeling its application in pose several challenges that are addressed this paper. Pacemakers should guarantee safe operations across large varieties heart conditions, which represented by an incomplete set timed automata models. A domain-specific abstraction rules developed can over-approximate timing behaviors or group models, such new introduced mostly physiologically meaningful. The serve as systematic method to cover conditions may not explicitly accounted initial systematically performed using models tree, obtain most concrete counter-example(s) correspond property violation. These counter-examples, along their context, then presented physician determine validity. proposed creates separation between steps requiring domain expertise (model creation definition) automated (rule application, checking, refinement). While illustrated pacemaker verification, more broadly applicable verification other devices.