Formal verification of a microfluidic device for blood cell separation

Amjad Gawanmeh, Anas Alazzam, Bobby Mathew

Research output: Contribution to journalArticlepeer-review

3 Scopus citations


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.

Original languageBritish English
Pages (from-to)227-235
Number of pages9
JournalScalable Computing
Issue number3
StatePublished - 2016


  • Blood cell separation
  • Medical system
  • Microfluidic device
  • Reliability analysis


Dive into the research topics of 'Formal verification of a microfluidic device for blood cell separation'. Together they form a unique fingerprint.

Cite this