Safety-critical medical device development using the UPP2SF model translation tool

Software-based control of life-critical embedded systems has become increasingly complex, and to a large extent has come to determine the safety of the human being. For example, implantable cardiac pacemakers have over 80,000 lines of code which are responsible for maintaining the heart within safe operating limits. As firmware-related recalls accounted for over 41% of the 600,000 devices recalled in the last decade, there is a need for rigorous model-driven design tools to generate verified code from verified software models. To this effect, we have developed the UPP2SF model-translation tool, which facilitates automatic conversion of verified models (in UPPAAL) to models that may be simulated and tested (in Simulink/Stateflow). We describe the translation rules that ensure correct model conversion, applicable to a large class of models. We demonstrate how UPP2SF is used in themodel-driven design of a pacemaker whosemodel is (a) designed and verified in UPPAAL (using timed automata), (b) automatically translated to Stateflow for simulation-based testing, and then (c) automatically generated into modular code for hardware-level integration testing of timing-related errors. In addition, we show how UPP2SF may be used for worst-case execution time estimation early in the design stage. Using UPP2SF, we demonstrate the value of integrated end-to-end modeling, verification, code-generation and testing process for complex software-controlled embedded systems. © 2014 ACM.

Safety and Use of Anticoagulation After Aortic Valve Replacement With Bioprostheses: A Meta-Analysis.

BACKGROUND: The American College of Cardiology guidelines recommend 3 months of anticoagulation after replacement of the aortic valve with a bioprosthesis. However, there remains great variability in the current clinical practice and conflicting results from clinical studies. To assist clinical decision making, we pooled the existing evidence to assess whether anticoagulation in the setting of a new bioprosthesis was associated with improved outcomes or greater risk of bleeding. METHODS AND RESULTS: We searched the PubMed database from the inception of these databases until April 2015 to identify original studies (observational studies or clinical trials) that assessed anticoagulation with warfarin in comparison with either aspirin or no antiplatelet or anticoagulant therapy. We included the studies if their outcomes included thromboembolism or stroke/transient ischemic attacks and bleeding events. Quality assessment was performed in accordance with the Newland Ottawa Scale, and random effects analysis was used to pool the data from the available studies. I(2) testing was done to assess the heterogeneity of the included studies. After screening through 170 articles, a total of 13 studies (cases=6431; controls=18210) were included in the final analyses. The use of warfarin was associated with a significantly increased risk of overall bleeding (odds ratio, 1.96; 95% confidence interval, 1.25-3.08; P<0.0001) or bleeding risk at 3 months (odds ratio, 1.92; 95% confidence interval, 1.10-3.34; P<0.0001) compared with aspirin or placebo. With regard to composite primary outcome variables (risk of venous thromboembolism, stroke, or transient ischemic attack) at 3 months, no significant difference was seen with warfarin (odds ratio, 1.13; 95% confidence interval, 0.82-1.56; P=0.67). Moreover, anticoagulation was also not shown to improve outcomes at time interval >3 months (odds ratio, 1.12; 95% confidence interval, 0.80-1.58; P=0.79). CONCLUSIONS: Contrary to the current guidelines, a meta-analysis of previous studies suggests that anticoagulation in the setting of an aortic bioprosthesis significantly increases bleeding risk without a favorable effect on thromboembolic events. Larger, randomized controlled studies should be performed to further guide this clinical practice.