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.

A Model of Lung Tumor Angiogenesis in a Biomimetic Poly(ethylene glycol)-based Hydrogel System

Tumor angiogenesis is critical to tumor growth and metastasis, yet much is unknown about the role vascular cells play in the tumor microenvironment. A major outstanding challenge associated with studying tumor angiogenesis is that existing preclinical models are limited in their recapitulation of in vivo cellular organization in 3D. This disparity highlights the need for better approaches to study the dynamic interplay of relevant cells and signaling molecules as they are organized in the tumor microenvironment. In this thesis, we combined 3D culture of lung adenocarcinoma cells with adjacent 3D microvascular cell culture in 2-layer cell-adhesive, proteolytically-degradable poly(ethylene glycol) (PEG)-based hydrogels to study tumor angiogenesis and the impacts of neovascularization on tumor cell behavior.

In initial studies, 344SQ cells, a highly metastatic, murine lung adenocarcinoma cell line, were characterized alone in 3D in PEG hydrogels. 344SQ cells formed spheroids in 3D culture and secreted proangiogenic growth factors into the conditioned media that significantly increased with exposure to transforming growth factor beta 1 (TGF-β1), a potent tumor progression-promoting factor. Vascular cells alone in hydrogels formed tubule networks with localized activated TGF-β1. To study cancer cell-vascular cell interactions, the engineered 2-layer tumor angiogenesis model with 344SQ and vascular cell layers was employed. Large, invasive 344SQ clusters developed at the interface between the layers, and were not evident further from the interface or in control hydrogels without vascular cells. A modified model with spatially restricted 344SQ and vascular cell layers confirmed that observed 344SQ cluster morphological changes required close proximity to vascular cells. Additionally, TGF-β1 inhibition blocked endothelial cell-driven 344SQ migration.

Two other lung adenocarcinoma cell lines were also explored in the tumor angiogenesis model: primary tumor-derived metastasis-incompetent, murine 393P cells and primary tumor-derived metastasis-capable human A549 cells. These lung cancer cells also formed spheroids in 3D culture and secreted proangiogenic growth factors into the conditioned media. Epithelial morphogenesis varied for the primary tumor-derived cell lines compared to 344SQ cells, with far less epithelial organization present in A549 spheroids. Additionally, 344SQ cells secreted the highest concentration of two of the three angiogenic growth factors assessed. This finding correlated to 344SQ exhibiting the most pronounced morphological response in the tumor angiogenesis model compared to the 393P and A549 cell lines.

Overall, this dissertation demonstrates the development of a novel 3D tumor angiogenesis model that was used to study vascular cell-cancer cell interactions in lung adenocarcinoma cell lines with varying metastatic capacities. Findings in this thesis have helped to elucidate the role of vascular cells in tumor progression and have identified differences in cancer cell behavior in vitro that correlate to metastatic capacity, thus highlighting the usefulness of this model platform for future discovery of novel tumor angiogenesis and tumor progression-promoting targets.