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 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.