Enhanced Biocompatibility of NiTi (Nitinol) Via Surface Treatment and Alloying

It is projected that by 2020, there will be 138 million Americans over 45, the age at which the increased incidence of heart diseases is documented. Many will require stents. This multi-billion dollar industry, with over 2 million patients worldwide, 15% of whom use Nitinol stents have experienced a decline in sales recently, due in part to thrombosis. It is a sudden blood clot that forms inside stents. As a result, the Food and Drug Administration and American Heart Association are calling for a new generation of stents, new designs and different alloys that are more adaptable to the arteries. The future of Nitinol therefore depends on a better understanding of the mechanisms by which Nitinol surfaces can be rendered stable and inert. In this investigation, binary and ternary Nitinol alloys were prepared and subjected to various surface treatments such as electropolishing (EP), magnetoelectropolishing (MEP) and water boiling & passivation (W&P). In vitro corrosion tests were conducted on Nitinol alloys in accordance with ASTM F 2129-08. The metal ions released into the electrolyte during corrosion tests were measured by Inductively Coupled Plasma Mass Spectroscopy (ICP-MS). Biocompatibility was assessed by observing the growth of human umbilical vein endothelial cells (HUVEC) on the surface of Nitinol alloys. Static and dynamic immersion tests were performed by immersing the Nitinol alloys in cell culture media and measuring the amount of metal ions released in solution. Sulforhodamine B (SRB) assays were performed to elucidate the effect of metal ions on the growth of HUVEC cells. The surfaces of the alloys were studied using Scanning Electron Microscopy (SEM) and X-ray Photoelectron Spectroscopy (XPS) respectively. Finally, wettability and surface energy were measured by Contact Angle Meter, whereas surface roughness was measured by Atomic Force Microscopy (AFM). All the surface treated alloys exhibited high resistance to corrosion when compared with untreated alloys. SRB assays revealed that Ni and Cu ions exhibited greater toxicity than Cr, Ta and Ti ions on HUVEC cells. EP and MEP alloys possessed relatively smooth surfaces and some were composed of nickel oxides instead of elemental nickel as determined by XPS. MEP exhibited lowest surface energy and lowest surface roughness.

Formal Modeling and Analysis Techniques for High Level Petri Nets

Petri Nets are a formal, graphical and executable modeling technique for the specification and analysis of concurrent and distributed systems and have been widely applied in computer science and many other engineering disciplines. Low level Petri nets are simple and useful for modeling control flows but not powerful enough to define data and system functionality. High level Petri nets (HLPNs) have been developed to support data and functionality definitions, such as using complex structured data as tokens and algebraic expressions as transition formulas. Compared to low level Petri nets, HLPNs result in compact system models that are easier to be understood. Therefore, HLPNs are more useful in modeling complex systems. There are two issues in using HLPNs - modeling and analysis. Modeling concerns the abstracting and representing the systems under consideration using HLPNs, and analysis deals with effective ways study the behaviors and properties of the resulting HLPN models. In this dissertation, several modeling and analysis techniques for HLPNs are studied, which are integrated into a framework that is supported by a tool. For modeling, this framework integrates two formal languages: a type of HLPNs called Predicate Transition Net (PrT Net) is used to model a system's behavior and a first-order linear time temporal logic (FOLTL) to specify the system's properties. The main contribution of this dissertation with regard to modeling is to develop a software tool to support the formal modeling capabilities in this framework. For analysis, this framework combines three complementary techniques, simulation, explicit state model checking and bounded model checking (BMC). Simulation is a straightforward and speedy method, but only covers some execution paths in a HLPN model. Explicit state model checking covers all the execution paths but suffers from the state explosion problem. BMC is a tradeoff as it provides a certain level of coverage while more efficient than explicit state model checking. The main contribution of this dissertation with regard to analysis is adapting BMC to analyze HLPN models and integrating the three complementary analysis techniques in a software tool to support the formal analysis capabilities in this framework. The SAMTools developed for this framework in this dissertation integrates three tools: PIPE+ for HLPNs behavioral modeling and simulation, SAMAT for hierarchical structural modeling and property specification, and PIPE+Verifier for behavioral verification.