Formal Verification of a Microfluidic Device for Blood Cell Separation
Journal Title: Scalable Computing: Practice and Experience - Year 2016, Vol 17, Issue 3
Abstract
Blood cell separation microdevices are designed in biomedical engineering for separation of cancer cells from blood. The movement of cancer cells particles in a continuous flow microfluidic device is a challenging problem since there are several forces incorporated. For instance, forces due to inertia, gravity, buoyancy, dielectrophoresis and virtual mass are accounted for in this system. Understanding the cell particle movement and behavior at high level of abstraction is necessary in order to avoid fundamental errors in the design of systems that can make use of this behavior. In this paper we use formal analysis in order to formalize and validate the movement of microparticles under DEP forces for blood cell separation microdevice. This is achieved by modeling the dynamic behavior that can predict the trajectory of microparticles as a transition state based system. The model is used to validate the correctness of the microdevice at early stages of the design process.
Authors and Affiliations
AMJAD GAWANMEH, ANAS ALAZZAM, BOBBY MATHEW
Keywords
Related Articles
- EP ID EP204681
- DOI 10.12694/scpe.v17i3.1182
- Views 17
- Downloads 0
Architecture of a Scalable Platform for Monitoring Multiple Big Data Frameworks
Latest advances in information technology and the widespread growth in different areas are producing large amounts of data. Consequently, in the past decade a large number of distributed platforms for storing and process...
A Self-healing Architecture based on RAINBOW for Industrial Usage
Over recent decades computer and software systems become more and more complex because of the applications and user requirements. The complexity makes the software systems more vulnerable to the error and bugs. Also, env...
Climate Applications in a Virtual Research Environment Platform
Previous atmospheric composition studies were based on extensive computer simulations carried out with good resolution using up-to-date modelling tools and detailed and reliable input data. The oncoming climate changes...
Formal Verification of a Microfluidic Device for Blood Cell Separation
Blood cell separation microdevices are designed in biomedical engineering for separation of cancer cells from blood. The movement of cancer cells particles in a continuous flow microfluidic device is a challenging proble...
Modelling and simulation of GPU processing in the MERPSYS environment
In this work, we evaluate an analytical GPU performance model based on Little's law, that expresses the kernel execution time in terms of latency bound, throughput bound, and achieved occupancy. We then combine it with t...